Theorem biimprcd 252

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 249	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimparc  483  ax12i  1988  moanimlem  2647  euan  2650  euanv  2653  eleq1a  2859  ceqsalgALT  3492  cgsexg  3500  cgsex2g  3501  cgsex4g  3502  spcegv  3558  spc2egv  3560  reu6  3691  csbiebt  3883  reusv2lem2  5358  ralxfrALT  5374  axprlem4  5385  sotr3  5598  opelxp  5685  ssrel  5757  ssrel2  5759  ssrelrel  5770  iss  6026  ordun  6454  fprb  7180  riotaclb  7396  iunpw  7756  limom  7864  funcnvuni  7915  fiunlem  7925  soxp  8111  tfrlem8  8357  oaordex  8529  eroveu  8796  fundmen  9014  nneneq  9176  onfin2  9187  dif1ennnALT  9223  unfilem1  9251  elirrv  9547  rankwflemb  9753  sornom  10236  isf32lem9  10320  axdc3lem2  10410  axdc4lem  10414  zorn2lem3  10457  zorn2lem7  10461  tskuni  10743  grur1a  10779  grothomex  10789  genpnnp  10965  ltaddpr  10994  reclem4pr  11010  supadd  12162  supmullem1  12164  uzin  12877  elfzmlbp  13646  isfinite4  14377  brfi1uzind  14523  swrdnd  14670  01sqrexlem6  15276  sqreulem  15389  fvprmselgcd1  17083  lubun  18549  lspsneq  21194  fvmptnn04ifb  22913  fbasfip  23930  alexsubALTlem2  24110  ovolunlem1  25561  dchrisum0flb  27576  nodmon  27716  noextendseq  27733  nocvxminlem  27849  brbtwn2  29108  axcontlem8  29174  isclwwlknx  30240  clwwlkel  30250  clwwlknwwlksnb  30259  wwlksext2clwwlk  30261  mdbr3  32502  mdbr4  32503  atssma  32583  atcvatlem  32590  ssrelf  32819  fnrelpredd  35389  nepss  36073  hfun  36533  nmulprop  36545  axtco2  36839  axtcond  36843  bj-ax12ig  37098  bj-alextruim  37114  bj-substw  37205  bj-axreprepsep  37565  finxpreclem2  37889  wl-eujustlem1  38096  indexdom  38238  fdc  38249  totbndss  38281  grpomndo  38379  iss2  38848  ax12eq  39570  ax12el  39571  lsatn0  39628  lsatcmp  39632  lsatcv0  39660  lfl1dim  39750  lfl1dim2N  39751  lkrss2N  39798  lub0N  39818  glb0N  39822  ispsubcl2N  40576  cdlemefrs29bpre0  41025  dihglblem2N  41923  dihglblem3N  41924  dochsnnz  42079  pm13.14  44990  tratrb  45117  ax6e2ndeq  45140  3impexpbicomVD  45437  tratrbVD  45441  equncomVD  45448  trsbcVD  45457  sbcssgVD  45463  csbingVD  45464  onfrALTVD  45471  csbsngVD  45473  csbxpgVD  45474  csbresgVD  45475  csbrngVD  45476  csbima12gALTVD  45477  csbunigVD  45478  csbfv12gALTVD  45479  con5VD  45480  hbimpgVD  45484  hbexgVD  45486  ax6e2ndeqVD  45489  supxrleubrnmpt  45985  suprleubrnmpt  46001  infxrgelbrnmpt  46033  usgrgrtrirex  48577  isassintop  48837  zgtp1leeq  49148