Theorem biimprcd 253

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 23	. 2 ⊢ (𝜒 → 𝜒)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibrcom 250	1 ⊢ (𝜒 → (𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimparc  485  ax12i  1999  moanimlem  2643  euan  2646  euanv  2649  eleq1a  2855  ceqsalgALT  3486  cgsexg  3494  cgsex2g  3495  cgsex4g  3496  spcegv  3551  spc2egv  3553  reu6  3683  csbiebt  3875  reusv2lem2  5360  ralxfrALT  5376  axprlem4  5387  sotr3  5596  opelxp  5683  ssrel  5755  ssrel2  5757  ssrelrel  5768  iss  6025  ordun  6458  fprb  7187  riotaclb  7406  iunpw  7768  limom  7876  funcnvuni  7927  fiunlem  7937  soxp  8124  tfrlem8  8370  oaordex  8544  eroveu  8811  fundmen  9037  nneneq  9199  onfin2  9210  dif1ennnALT  9246  unfilem1  9275  elirrv  9569  rankwflemb  9775  hfunOLD  9890  sornom  10326  isf32lem9  10410  axdc3lem2  10500  axdc4lem  10504  zorn2lem3  10547  zorn2lem7  10551  tskuni  10839  grur1a  10875  grothomex  10885  genpnnp  11061  ltaddpr  11090  reclem4pr  11106  supadd  12254  supmullem1  12256  uzin  12970  elfzmlbp  13741  isfinite4  14473  brfi1uzind  14620  swrdnd  14771  01sqrexlem6  15381  sqreulem  15494  fvprmselgcd1  17184  lubun  18650  lspsneq  21361  fvmptnn04ifb  23130  fbasfip  24148  alexsubALTlem2  24328  ovolunlem1  25779  dchrisum0flb  27800  nodmon  27940  noextendseq  27957  nocvxminlem  28073  brbtwn2  29416  axcontlem8  29482  isclwwlknx  30560  clwwlkel  30570  clwwlknwwlksnb  30579  wwlksext2clwwlk  30581  mdbr3  32832  mdbr4  32833  atssma  32913  atcvatlem  32920  ssrelf  33142  fnrelpredd  35650  nepss  36404  nmulprop  36861  axtco2  37184  axtcond  37188  bj-ax12ig  37442  bj-alextruim  37458  bj-substw  37549  bj-axreprepsep  37911  finxpreclem2  38233  wl-eujustlem1  38440  indexdom  38588  fdc  38599  totbndss  38631  grpomndo  38729  iss2  39196  ax12eq  39918  ax12el  39919  lsatn0  39976  lsatcmp  39980  lsatcv0  40008  lfl1dim  40098  lfl1dim2N  40099  lkrss2N  40146  lub0N  40166  glb0N  40170  ispsubcl2N  40924  cdlemefrs29bpre0  41373  dihglblem2N  42271  dihglblem3N  42272  dochsnnz  42427  pm13.14  45337  tratrb  45463  ax6e2ndeq  45486  3impexpbicomVD  45783  tratrbVD  45787  equncomVD  45794  trsbcVD  45803  sbcssgVD  45809  csbingVD  45810  onfrALTVD  45817  csbsngVD  45819  csbxpgVD  45820  csbresgVD  45821  csbrngVD  45822  csbima12gALTVD  45823  csbunigVD  45824  csbfv12gALTVD  45825  con5VD  45826  hbimpgVD  45830  hbexgVD  45832  ax6e2ndeqVD  45835  supxrleubrnmpt  46338  suprleubrnmpt  46354  infxrgelbrnmpt  46386  usgrgrtrirex  48970  isassintop  49229  zgtp1leeq  49555