Theorem biimpd 151

Description: Deduce an implication from a logical equivalence.

Hypothesis

Ref	Expression
biimpd.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
biimpd	⊢ (φ → (ψ → χ))

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 ⊢ (φ → (ψ ↔ χ))
2		bi1 146	. 2 ⊢ ((ψ ↔ χ) → (ψ → χ))
3	1, 2	syl 10	1 ⊢ (φ → (ψ → χ))

Syntax hints:   → wi 3   ↔ wb 144

This theorem is referenced by:  biimpcd 153  mpbii 191  mpbid 193  sylibd 200  sylbid 201  syl5bi 206  syl6bi 212  biimpa 416  bitrd 531  ibi 595  anbi2d 619  mtbird 720  mtbiri 722  consensus 772  dral1 1191  chvar 1204  sbequi 1265  a4v 1310  2eu3 1491  eqrdav 1517  ceqsalg 1871  vtoclf 1887  vtocl2 1889  vtocl3 1890  cla4gf 1906  ra4sbc 2047  iununi 2686  ordtr2 3019  trsuc 3056  ordsssuc2 3060  onmindif 3061  reuuni1 3106  elpwunsn 3135  onint 3152  oneqmin 3162  ordsucelsuc 3178  ordunisuc2 3198  tfinds 3212  tfindsg 3213  limom 3233  findsg 3245  relop 3365  unixp0 3623  tz6.12i 3852  chfnrn 3916  exfo 3936  ffnfv 3942  funiunfv 3980  isomin 4013  f1oweALT 4020  canth 4205  oaordi 4316  oawordri 4320  oaordex 4328  oalimcl 4330  oarec 4332  omwordi 4338  oewordi 4354  oelim2 4358  dom2d 4545  ac6sfilem3 4590  nneneq 4659  pssnn 4681  unfilem2 4695  suc11reg 4750  zorn2lem7 4940  unidom 4954  uniimadom 4956  cardlim 5001  alephnbtwn 5018  alephord2i 5027  cardaleph 5035  alephiso 5042  cflim 5059  mulcanpi 5181  genpcd 5263  genpnmax 5264  prlem934a 5291  prlem934b 5292  prlem934 5293  ltexprlem4 5299  reclem4pr 5313  suplem2pr 5316  suppsr2 5377  pre-axltadd 5443  ltletr 5678  xrltletr 5717  addgegt0i 5754  mul0ori 5846  divne0 5875  prodgt02 5967  prodge02 5969  lemul1a 5981  lemul1aOLD 5982  mulgt1 5989  divgt0 5999  divge0 6000  ledivp1i 6051  ltdivp1i 6052  nominpos 6189  supxr 6249  elnn0nn 6339  btwnnz 6363  dfuzi 6373  uzindOLD 6379  zmax 6392  qbtwnre 6418  flval2 6437  flval3 6438  iccsupr 6525  icoshft 6535  icoshftf1oii 6536  fzen 6622  fsequb2 6655  fseqsupcl 6656  fseqsupubi 6657  expwordi 6800  expword2i 6802  sq01 6848  cjre 7011  seq1ublem 7114  cvg1 7124  bccl2 7174  climaddc2 7322  climsqueeze 7343  climsqueeze2 7344  expcnvlem6 7436  georeclim 7445  cvgratlem1ALT 7452  cvgratlem1 7455  cncffvelrnOLD 7472  mulc1cncf 7484  ivthlem6 7491  ivthlem7 7492  efcltlem1 7509  reeff1 7618  reeff1o 7634  ruclem24 7745  bastop1 7854  clsval2 7895  0ntr 7912  islpi 7959  cnpco 7979  cncnplem2 7985  cncnplem4 7987  sncld 7997  metxp 8044  metequiv 8091  caussi 8165  metelcls 8176  metcn4i 8183  xplmi 8184  xpcn 8187  lmcau 8207  bcthlem16 8225  gxid 8329  grplactf1o 8339  issubg 8358  nvlmle 8580  vacnlem6 8587  hlipgt0 8878  efif1lem3 9004  ocin 9445  ocnel 9446  projlem15 9476  shmodsi 9638  pjmf1 9939  unopf1o 10120  staddi 10454  stadd3i 10456  mdi 10503  dmdmd 10508  dmdi 10510  dmdbr2 10511  dmdbr3 10513  dmdbr4 10514  dmdi4 10515  mdsl1i 10529  superpos 10562  cvbr3i 10575  atssma 10587  atcv1 10589  atomli 10591  irredlem1 10599  elghomlem2 10668  nndivsub 10706  uninqs 10730  fiiu 10738  ficli 10756  domrngref 10764  domintreflem 10766  sqpeq 10786  njtlc 10804  restidsing 10805  prj1 10809  unpde2eg2 10825  islatalg 10831  fiiu2 10852  infi 10854  inpc 10867  dominc 10870  rninc 10871  dupos2 10879  lteqtpos 10880  tostos 10883  toplat 10884  opidon 10898  opidon2 10900  grpmnd 10933  ununr 10955  on1el4 10963  uznzr 10967  dvrunz 10970  cdrci 10994  bsi 10995  truni1 10999  truni3 11001  cnrsfin 11012  cnrscoa 11013  mapdiscn 11014  nsn 11017  cnvhmphb 11032  hmphsyma 11034  hmphtr 11037  homcard 11045  subtopsin2 11067  cnfilca 11088  rcfpfillem2 11090  rcfpfillem6 11094  bwt2 11123  usinuniop 11128  altretop 11144  dmse1 11146  ltsubpostb 11150  ltaddpos2tb 11151  iintlem1 11155  rdmob 11202  eqidob 11250  ismonc 11269  cmpmon 11270  idmon 11272  iepiclem 11278  isepic 11279  fmp 11294  cptclsscpt 11489  hscptsscld 11491  compfipin0 11493  alexsublem3 11498  alexsublem4 11499  alexsub 11500  topfneec2 11563  comppfsc 11578  fnejoin1 11591  fnejoin2 11592  ist1-2 11603  t1sep 11607  isnrm2 11613  nrmsep2 11616  fbfgss 11640  filrn 11643  isufil2 11650  elfilmap3 11692  fmfnfmlem4 11703  fmfnfm 11704  brabg2 11788  elpreima 11792  morex 11804  f1elima 11818  dif1card 11835  findcard 11836  fimax 11837  fixp 11840  fipreima 11848  divexp 11859  fzm1 11867  absz 11868  sdclem1 11875  sdclem2 11876  sdc 11877  incsequz2 11880  fsum00 11883  fsumlt1 11894  blhalf 11911  mettrifi 11912  mettrifi2 11913  geomcau 11914  iccshftri 11923  iccshftli 11925  iccdili 11927  icccntri 11929  ishomeo2 11957  lmtlm 11969  tx1cn 11976  tx2cn 11977  txcn 11979  sstotbnd 11992  isbnd3 11997  totbndbnd 12000  ismtyhmeo 12007  heiborlem1 12011  heiborlem13 12023  heiborlem16 12026  heiborlem23 12033  heiborlem30 12040  heiborlem32 12042  rrnmet 12072  rrncms 12075  rrntotbnd 12078  isphtpc2 12102

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145

Copyright terms: Public domain