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  1966  moanimlem  2611  euan  2614  euanv  2617  eleq1a  2823  ceqsalgALT  3484  cgsexg  3492  cgsex2g  3493  cgsex4g  3494  cgsex4gOLD  3495  ceqsexOLD  3497  spcegv  3563  spc2egv  3565  reu6  3697  csbiebt  3891  dfiin2g  4996  reusv2lem2  5354  ralxfrALT  5370  axprlem4  5381  sotr3  5587  opelxp  5674  ssrel  5745  ssrelOLD  5746  ssrel2  5748  ssrelrel  5759  iss  6006  ordun  6438  fprb  7168  riotaclb  7385  iunpw  7747  limom  7858  funcnvuni  7908  fiunlem  7920  soxp  8108  tfrlem8  8352  oaordex  8522  eroveu  8785  fundmen  9002  nneneq  9170  onfin2  9180  dif1ennnALT  9222  unfilem1  9254  rankwflemb  9746  sornom  10230  isf32lem9  10314  axdc3lem2  10404  axdc4lem  10408  zorn2lem3  10451  zorn2lem7  10455  tskuni  10736  grur1a  10772  grothomex  10782  genpnnp  10958  ltaddpr  10987  reclem4pr  11003  supadd  12151  supmullem1  12153  uzin  12833  elfzmlbp  13600  isfinite4  14327  brfi1uzind  14473  swrdnd  14619  01sqrexlem6  15213  sqreulem  15326  fvprmselgcd1  17016  lubun  18474  lspsneq  21032  fvmptnn04ifb  22738  fbasfip  23755  alexsubALTlem2  23935  ovolunlem1  25398  dchrisum0flb  27421  nodmon  27562  noextendseq  27579  nocvxminlem  27689  brbtwn2  28832  axcontlem8  28898  isclwwlknx  29965  clwwlkel  29975  clwwlknwwlksnb  29984  wwlksext2clwwlk  29986  mdbr3  32226  mdbr4  32227  atssma  32307  atcvatlem  32314  ssrelf  32543  fnrelpredd  35079  nepss  35705  hfun  36166  bj-ax12ig  36624  bj-substw  36710  finxpreclem2  37378  indexdom  37728  fdc  37739  totbndss  37771  grpomndo  37869  iss2  38326  ax12eq  38934  ax12el  38935  lsatn0  38992  lsatcmp  38996  lsatcv0  39024  lfl1dim  39114  lfl1dim2N  39115  lkrss2N  39162  lub0N  39182  glb0N  39186  ispsubcl2N  39941  cdlemefrs29bpre0  40390  dihglblem2N  41288  dihglblem3N  41289  dochsnnz  41444  pm13.14  44398  tratrb  44526  ax6e2ndeq  44549  3impexpbicomVD  44846  tratrbVD  44850  equncomVD  44857  trsbcVD  44866  sbcssgVD  44872  csbingVD  44873  onfrALTVD  44880  csbsngVD  44882  csbxpgVD  44883  csbresgVD  44884  csbrngVD  44885  csbima12gALTVD  44886  csbunigVD  44887  csbfv12gALTVD  44888  con5VD  44889  hbimpgVD  44893  hbexgVD  44895  ax6e2ndeqVD  44898  supxrleubrnmpt  45402  suprleubrnmpt  45418  infxrgelbrnmpt  45450  usgrgrtrirex  47946  isassintop  48195  zgtp1leeq  48507