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  2621  euan  2624  euanv  2627  eleq1a  2839  ceqsalgALT  3526  cgsexg  3536  cgsex2g  3537  cgsex4g  3538  cgsex4gOLD  3539  ceqsexOLD  3541  ceqsexvOLD  3543  spcegv  3610  spc2egv  3612  reu6  3748  csbiebt  3951  dfiin2g  5055  reusv2lem2  5417  ralxfrALT  5433  sotr3  5648  opelxp  5736  ssrel  5806  ssrelOLD  5807  ssrel2  5809  ssrelrel  5820  iss  6064  ordun  6499  fprb  7231  riotaclb  7446  iunpw  7806  limom  7919  funcnvuni  7972  fiunlem  7982  soxp  8170  tfrlem8  8440  oaordex  8614  eroveu  8870  fundmen  9096  nneneq  9272  nneneqOLD  9284  onfin2  9294  dif1ennnALT  9339  unfilem1  9371  rankwflemb  9862  sornom  10346  isf32lem9  10430  axdc3lem2  10520  axdc4lem  10524  zorn2lem3  10567  zorn2lem7  10571  tskuni  10852  grur1a  10888  grothomex  10898  genpnnp  11074  ltaddpr  11103  reclem4pr  11119  supadd  12263  supmullem1  12265  uzin  12943  elfzmlbp  13696  isfinite4  14411  brfi1uzind  14557  swrdnd  14702  01sqrexlem6  15296  sqreulem  15408  fvprmselgcd1  17092  lubun  18585  lspsneq  21147  fvmptnn04ifb  22878  fbasfip  23897  alexsubALTlem2  24077  ovolunlem1  25551  dchrisum0flb  27572  nodmon  27713  noextendseq  27730  nocvxminlem  27840  brbtwn2  28938  axcontlem8  29004  isclwwlknx  30068  clwwlkel  30078  clwwlknwwlksnb  30087  wwlksext2clwwlk  30089  mdbr3  32329  mdbr4  32330  atssma  32410  atcvatlem  32417  ssrelf  32637  fnrelpredd  35065  nepss  35680  hfun  36142  bj-ax12ig  36602  bj-substw  36688  finxpreclem2  37356  indexdom  37694  fdc  37705  totbndss  37737  grpomndo  37835  iss2  38300  ax12eq  38897  ax12el  38898  lsatn0  38955  lsatcmp  38959  lsatcv0  38987  lfl1dim  39077  lfl1dim2N  39078  lkrss2N  39125  lub0N  39145  glb0N  39149  ispsubcl2N  39904  cdlemefrs29bpre0  40353  dihglblem2N  41251  dihglblem3N  41252  dochsnnz  41407  pm13.14  44378  tratrb  44507  ax6e2ndeq  44530  3impexpbicomVD  44828  tratrbVD  44832  equncomVD  44839  trsbcVD  44848  sbcssgVD  44854  csbingVD  44855  onfrALTVD  44862  csbsngVD  44864  csbxpgVD  44865  csbresgVD  44866  csbrngVD  44867  csbima12gALTVD  44868  csbunigVD  44869  csbfv12gALTVD  44870  con5VD  44871  hbimpgVD  44875  hbexgVD  44877  ax6e2ndeqVD  44880  supxrleubrnmpt  45321  suprleubrnmpt  45337  infxrgelbrnmpt  45369  usgrgrtrirex  47799  isassintop  47933  zgtp1leeq  48250