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  2619  euan  2622  euanv  2625  eleq1a  2832  ceqsalgALT  3479  cgsexg  3487  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  spcegv  3553  spc2egv  3555  reu6  3686  csbiebt  3880  dfiin2g  4988  reusv2lem2  5348  ralxfrALT  5364  axprlem4  5375  sotr3  5583  opelxp  5670  ssrel  5742  ssrel2  5744  ssrelrel  5755  iss  6004  ordun  6433  fprb  7152  riotaclb  7368  iunpw  7728  limom  7836  funcnvuni  7886  fiunlem  7898  soxp  8083  tfrlem8  8327  oaordex  8497  eroveu  8763  fundmen  8982  nneneq  9144  onfin2  9155  dif1ennnALT  9191  unfilem1  9219  rankwflemb  9719  sornom  10201  isf32lem9  10285  axdc3lem2  10375  axdc4lem  10379  zorn2lem3  10422  zorn2lem7  10426  tskuni  10708  grur1a  10744  grothomex  10754  genpnnp  10930  ltaddpr  10959  reclem4pr  10975  supadd  12124  supmullem1  12126  uzin  12801  elfzmlbp  13569  isfinite4  14299  brfi1uzind  14445  swrdnd  14592  01sqrexlem6  15184  sqreulem  15297  fvprmselgcd1  16987  lubun  18452  lspsneq  21094  fvmptnn04ifb  22812  fbasfip  23829  alexsubALTlem2  24009  ovolunlem1  25471  dchrisum0flb  27494  nodmon  27635  noextendseq  27652  nocvxminlem  27767  brbtwn2  28996  axcontlem8  29062  isclwwlknx  30129  clwwlkel  30139  clwwlknwwlksnb  30148  wwlksext2clwwlk  30150  mdbr3  32391  mdbr4  32392  atssma  32472  atcvatlem  32479  ssrelf  32711  fnrelpredd  35274  nepss  35940  hfun  36400  bj-ax12ig  36883  bj-alextruim  36899  bj-substw  36990  bj-axreprepsep  37350  finxpreclem2  37672  wl-eujustlem1  37872  indexdom  38014  fdc  38025  totbndss  38057  grpomndo  38155  iss2  38624  ax12eq  39346  ax12el  39347  lsatn0  39404  lsatcmp  39408  lsatcv0  39436  lfl1dim  39526  lfl1dim2N  39527  lkrss2N  39574  lub0N  39594  glb0N  39598  ispsubcl2N  40352  cdlemefrs29bpre0  40801  dihglblem2N  41699  dihglblem3N  41700  dochsnnz  41855  pm13.14  44794  tratrb  44921  ax6e2ndeq  44944  3impexpbicomVD  45241  tratrbVD  45245  equncomVD  45252  trsbcVD  45261  sbcssgVD  45267  csbingVD  45268  onfrALTVD  45275  csbsngVD  45277  csbxpgVD  45278  csbresgVD  45279  csbrngVD  45280  csbima12gALTVD  45281  csbunigVD  45282  csbfv12gALTVD  45283  con5VD  45284  hbimpgVD  45288  hbexgVD  45290  ax6e2ndeqVD  45293  supxrleubrnmpt  45793  suprleubrnmpt  45809  infxrgelbrnmpt  45841  usgrgrtrirex  48339  isassintop  48599  zgtp1leeq  48910