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  1968  moanimlem  2617  euan  2620  euanv  2623  eleq1a  2830  ceqsalgALT  3476  cgsexg  3484  cgsex2g  3485  cgsex4g  3486  cgsex4gOLD  3487  spcegv  3550  spc2egv  3552  reu6  3683  csbiebt  3877  dfiin2g  4985  reusv2lem2  5343  ralxfrALT  5359  axprlem4  5370  sotr3  5572  opelxp  5659  ssrel  5731  ssrel2  5733  ssrelrel  5744  iss  5993  ordun  6422  fprb  7140  riotaclb  7356  iunpw  7716  limom  7824  funcnvuni  7874  fiunlem  7886  soxp  8071  tfrlem8  8315  oaordex  8485  eroveu  8751  fundmen  8970  nneneq  9132  onfin2  9143  dif1ennnALT  9179  unfilem1  9207  rankwflemb  9707  sornom  10189  isf32lem9  10273  axdc3lem2  10363  axdc4lem  10367  zorn2lem3  10410  zorn2lem7  10414  tskuni  10696  grur1a  10732  grothomex  10742  genpnnp  10918  ltaddpr  10947  reclem4pr  10963  supadd  12112  supmullem1  12114  uzin  12789  elfzmlbp  13557  isfinite4  14287  brfi1uzind  14433  swrdnd  14580  01sqrexlem6  15172  sqreulem  15285  fvprmselgcd1  16975  lubun  18440  lspsneq  21079  fvmptnn04ifb  22797  fbasfip  23814  alexsubALTlem2  23994  ovolunlem1  25456  dchrisum0flb  27479  nodmon  27620  noextendseq  27637  nocvxminlem  27752  brbtwn2  28959  axcontlem8  29025  isclwwlknx  30092  clwwlkel  30102  clwwlknwwlksnb  30111  wwlksext2clwwlk  30113  mdbr3  32353  mdbr4  32354  atssma  32434  atcvatlem  32441  ssrelf  32673  fnrelpredd  35226  nepss  35891  hfun  36351  bj-ax12ig  36809  bj-substw  36896  finxpreclem2  37564  wl-eujustlem1  37762  indexdom  37904  fdc  37915  totbndss  37947  grpomndo  38045  iss2  38514  ax12eq  39236  ax12el  39237  lsatn0  39294  lsatcmp  39298  lsatcv0  39326  lfl1dim  39416  lfl1dim2N  39417  lkrss2N  39464  lub0N  39484  glb0N  39488  ispsubcl2N  40242  cdlemefrs29bpre0  40691  dihglblem2N  41589  dihglblem3N  41590  dochsnnz  41745  pm13.14  44687  tratrb  44814  ax6e2ndeq  44837  3impexpbicomVD  45134  tratrbVD  45138  equncomVD  45145  trsbcVD  45154  sbcssgVD  45160  csbingVD  45161  onfrALTVD  45168  csbsngVD  45170  csbxpgVD  45171  csbresgVD  45172  csbrngVD  45173  csbima12gALTVD  45174  csbunigVD  45175  csbfv12gALTVD  45176  con5VD  45177  hbimpgVD  45181  hbexgVD  45183  ax6e2ndeqVD  45186  supxrleubrnmpt  45687  suprleubrnmpt  45703  infxrgelbrnmpt  45735  usgrgrtrirex  48233  isassintop  48493  zgtp1leeq  48804