Theorem biimpcd 248

Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimpcd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpcd	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibcom 244	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 205

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  biimpac  479  axc16i  2435  nelneq  2857  nelneq2  2858  r19.35  3108  nssne1  4044  nssne2  4045  psssstr  4106  prproe  4906  iununi  5102  disjiun  5135  nbrne1  5167  nbrne2  5168  propeqop  5507  mosubopt  5510  relsnb  5802  relcnvtrg  6265  reuop  6292  dfpo2  6295  tz7.7  6390  suctr  6450  tz6.12i  6919  ssimaex  6976  chfnrn  7050  fvn0ssdmfun  7076  ffnfv  7120  f1elima  7264  elovmpt3rab1  7668  limsssuc  7841  nnsuc  7875  peano5  7886  peano5OLD  7887  dftpos4  8232  odi  8581  pssnn  9170  fineqvlem  9264  pssnnOLD  9267  ordunifi  9295  wdom2d  9577  r1pwss  9781  alephval3  10107  infdif  10206  cff1  10255  cofsmo  10266  axdc3lem2  10448  zorn2lem6  10498  cfpwsdom  10581  prub  10991  prnmadd  10994  1re  11218  letr  11312  dedekindle  11382  addrid  11398  negf1o  11648  negfi  12167  xrletr  13141  0fz1  13525  elfzmlbp  13616  leisorel  14425  elss2prb  14452  exprelprel  14454  fi1uzind  14462  swrdnd  14608  sqrmo  15202  isprm2  16623  nprmdvds1  16647  oddprmdvds  16840  catsubcat  17793  funcestrcsetclem8  18103  funcestrcsetclem9  18104  fthestrcsetc  18106  fullestrcsetc  18107  funcsetcestrclem9  18119  fthsetcestrc  18121  fullsetcestrc  18122  pltletr  18300  mgmpropd  18576  issstrmgm  18578  mgm2nsgrplem3  18837  sgrp2nmndlem3  18842  fvcosymgeq  19338  sylow2alem2  19527  islss  20689  gzrngunitlem  21210  pjdm2  21485  assamulgscmlem2  21673  gsumply1subr  21976  dmatmul  22219  decpmatmullem  22493  monmat2matmon  22546  chpscmat  22564  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  isclo2  22812  fbasfip  23592  ufileu  23643  alexsubALTlem2  23772  cnextcn  23791  metustbl  24295  scutbdaybnd2lim  27543  addsprop  27686  elntg2  28498  ushgredgedg  28741  ushgredgedgloop  28743  edgnbusgreu  28879  nb3grprlem1  28892  cusgrfilem1  28967  cusgrfilem2  28968  umgr2v2evtxel  29034  wlkcompim  29144  usgr2pth  29276  usgr2trlncrct  29315  wwlknp  29352  wlkiswwlks2lem3  29380  wlkiswwlksupgr2  29386  wlklnwwlkln2lem  29391  wwlksnext  29402  2pthdlem1  29439  umgr2adedgwlkonALT  29456  umgr2wlkon  29459  elwspths2spth  29476  rusgr0edg  29482  clwlkclwwlklem2a1  29500  clwlkclwwlklem2a  29506  clwwisshclwwslem  29522  loopclwwlkn1b  29550  clwwlkel  29554  clwwlkext2edg  29564  hashecclwwlkn1  29585  umgrhashecclwwlk  29586  clwwlknonwwlknonb  29614  uhgr3cyclexlem  29689  upgr4cycl4dv4e  29693  eupth2lem3lem4  29739  frgruhgr0v  29772  numclwwlk1lem2f1  29865  numclwlk2lem2f  29885  numclwlk2lem2f1o  29887  frgrogt3nreg  29905  5oalem6  31167  eigorthi  31345  adjbd1o  31593  dmdbr7ati  31932  fmla1  34664  satffunlem2lem2  34683  fundmpss  35030  funbreq  35033  idinside  35348  bj-opelidres  36345  bj-eldiag2  36361  bj-fvimacnv0  36470  poimirlem32  36823  sdclem2  36913  fdc1  36917  ismgmOLD  37021  lsatcvatlem  38222  atnle  38490  cvratlem  38595  ispsubcl2N  39121  trlord  39743  diaelrnN  40219  cdlemm10N  40292  dochexmidlem7  40640  fsuppind  41464  3impexpbicom  43542  sbcim2g  43601  suctrALT2VD  43899  suctrALT2  43900  3impexpVD  43919  3impexpbicomVD  43920  sbcim2gVD  43938  csbeq2gVD  43955  csbsngVD  43956  ax6e2ndeqVD  43972  2sb5ndVD  43973  infxrunb3rnmpt  44437  lptioo2  44646  lptioo1  44647  funressnfv  46052  ffnafv  46178  tz6.12i-afv2  46250  iccpartiltu  46389  iccpartigtl  46390  icceuelpartlem  46402  fargshiftfo  46409  ichnreuop  46439  reupr  46489  bgoldbtbndlem2  46773  rngcinv  46968  rngcinvALTV  46980  srhmsubc  47063  srhmsubcALTV  47081  nnolog2flm1  47364  prelrrx2b  47488  rrxlinec  47510  eenglngeehlnm  47513