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  1998  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  5599  opelxp  5686  ssrel  5758  ssrel2  5760  ssrelrel  5771  iss  6026  ordun  6469  fprb  7199  riotaclb  7418  iunpw  7785  limom  7893  funcnvuni  7944  fiunlem  7954  soxp  8141  tfrlem8  8392  oaordex  8566  eroveu  8833  fundmen  9059  nneneq  9221  onfin2  9232  dif1ennnALT  9268  unfilem1  9297  elirrv  9591  rankwflemb  9800  rankwflembOLD  9801  hfunOLD  9919  sornom  10355  isf32lem9  10439  axdc3lem2  10529  axdc4lem  10533  zorn2lem3  10576  zorn2lem7  10580  tskuni  10868  grur1a  10904  grothomex  10914  genpnnp  11090  ltaddpr  11119  reclem4pr  11135  supadd  12285  supmullem1  12287  uzin  13001  elfzmlbp  13773  isfinite4  14506  brfi1uzind  14653  swrdnd  14804  01sqrexlem6  15414  sqreulem  15527  fvprmselgcd1  17223  lubun  18689  lspsneq  21400  fvmptnn04ifb  23169  fbasfip  24187  alexsubALTlem2  24367  ovolunlem1  25818  dchrisum0flb  27837  nodmon  28007  noextendseq  28024  nocvxminlem  28140  brbtwn2  29483  axcontlem8  29549  isclwwlknx  30627  clwwlkel  30637  clwwlknwwlksnb  30646  wwlksext2clwwlk  30648  mdbr3  32899  mdbr4  32900  atssma  32980  atcvatlem  32987  ssrelf  33209  fnrelpredd  35720  nepss  36483  nmulprop  36939  axtco2  37262  axtcond  37266  bj-ax12ig  37520  bj-alextruim  37536  bj-substw  37627  bj-axreprepsep  37991  finxpreclem2  38314  wl-eujustlem1  38521  indexdom  38669  fdc  38680  totbndss  38712  grpomndo  38810  iss2  39277  ax12eq  39999  ax12el  40000  lsatn0  40057  lsatcmp  40061  lsatcv0  40089  lfl1dim  40179  lfl1dim2N  40180  lkrss2N  40227  lub0N  40247  glb0N  40251  ispsubcl2N  41005  cdlemefrs29bpre0  41454  dihglblem2N  42352  dihglblem3N  42353  dochsnnz  42508  pm13.14  45393  tratrb  45519  ax6e2ndeq  45542  3impexpbicomVD  45839  tratrbVD  45843  equncomVD  45850  trsbcVD  45859  sbcssgVD  45865  csbingVD  45866  onfrALTVD  45873  csbsngVD  45875  csbxpgVD  45876  csbresgVD  45877  csbrngVD  45878  csbima12gALTVD  45879  csbunigVD  45880  csbfv12gALTVD  45881  con5VD  45882  hbimpgVD  45886  hbexgVD  45888  ax6e2ndeqVD  45891  supxrleubrnmpt  46416  suprleubrnmpt  46432  infxrgelbrnmpt  46464  usgrgrtrirex  49048  isassintop  49307  zgtp1leeq  49633