Theorem biimprcd 250

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

Hypothesis

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

Assertion

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

Proof of Theorem biimprcd

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimparc  479  ax12i  1966  moanimlem  2611  euan  2614  euanv  2617  eleq1a  2823  ceqsalgALT  3481  cgsexg  3489  cgsex2g  3490  cgsex4g  3491  cgsex4gOLD  3492  ceqsexOLD  3494  spcegv  3560  spc2egv  3562  reu6  3694  csbiebt  3888  dfiin2g  4991  reusv2lem2  5349  ralxfrALT  5365  axprlem4  5376  sotr3  5580  opelxp  5667  ssrel  5737  ssrel2  5739  ssrelrel  5750  iss  5995  ordun  6426  fprb  7150  riotaclb  7367  iunpw  7727  limom  7838  funcnvuni  7888  fiunlem  7900  soxp  8085  tfrlem8  8329  oaordex  8499  eroveu  8762  fundmen  8979  nneneq  9147  onfin2  9157  dif1ennnALT  9198  unfilem1  9230  rankwflemb  9722  sornom  10206  isf32lem9  10290  axdc3lem2  10380  axdc4lem  10384  zorn2lem3  10427  zorn2lem7  10431  tskuni  10712  grur1a  10748  grothomex  10758  genpnnp  10934  ltaddpr  10963  reclem4pr  10979  supadd  12127  supmullem1  12129  uzin  12809  elfzmlbp  13576  isfinite4  14303  brfi1uzind  14449  swrdnd  14595  01sqrexlem6  15189  sqreulem  15302  fvprmselgcd1  16992  lubun  18456  lspsneq  21064  fvmptnn04ifb  22771  fbasfip  23788  alexsubALTlem2  23968  ovolunlem1  25431  dchrisum0flb  27454  nodmon  27595  noextendseq  27612  nocvxminlem  27723  brbtwn2  28885  axcontlem8  28951  isclwwlknx  30015  clwwlkel  30025  clwwlknwwlksnb  30034  wwlksext2clwwlk  30036  mdbr3  32276  mdbr4  32277  atssma  32357  atcvatlem  32364  ssrelf  32593  fnrelpredd  35072  nepss  35698  hfun  36159  bj-ax12ig  36617  bj-substw  36703  finxpreclem2  37371  indexdom  37721  fdc  37732  totbndss  37764  grpomndo  37862  iss2  38319  ax12eq  38927  ax12el  38928  lsatn0  38985  lsatcmp  38989  lsatcv0  39017  lfl1dim  39107  lfl1dim2N  39108  lkrss2N  39155  lub0N  39175  glb0N  39179  ispsubcl2N  39934  cdlemefrs29bpre0  40383  dihglblem2N  41281  dihglblem3N  41282  dochsnnz  41437  pm13.14  44391  tratrb  44519  ax6e2ndeq  44542  3impexpbicomVD  44839  tratrbVD  44843  equncomVD  44850  trsbcVD  44859  sbcssgVD  44865  csbingVD  44866  onfrALTVD  44873  csbsngVD  44875  csbxpgVD  44876  csbresgVD  44877  csbrngVD  44878  csbima12gALTVD  44879  csbunigVD  44880  csbfv12gALTVD  44881  con5VD  44882  hbimpgVD  44886  hbexgVD  44888  ax6e2ndeqVD  44891  supxrleubrnmpt  45395  suprleubrnmpt  45411  infxrgelbrnmpt  45443  usgrgrtrirex  47942  isassintop  48191  zgtp1leeq  48503