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  1967  moanimlem  2613  euan  2616  euanv  2619  eleq1a  2826  ceqsalgALT  3473  cgsexg  3481  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  spcegv  3547  spc2egv  3549  reu6  3680  csbiebt  3874  dfiin2g  4979  reusv2lem2  5335  ralxfrALT  5351  axprlem4  5362  sotr3  5563  opelxp  5650  ssrel  5722  ssrel2  5724  ssrelrel  5735  iss  5983  ordun  6412  fprb  7128  riotaclb  7344  iunpw  7704  limom  7812  funcnvuni  7862  fiunlem  7874  soxp  8059  tfrlem8  8303  oaordex  8473  eroveu  8736  fundmen  8953  nneneq  9115  onfin2  9125  dif1ennnALT  9161  unfilem1  9189  rankwflemb  9686  sornom  10168  isf32lem9  10252  axdc3lem2  10342  axdc4lem  10346  zorn2lem3  10389  zorn2lem7  10393  tskuni  10674  grur1a  10710  grothomex  10720  genpnnp  10896  ltaddpr  10925  reclem4pr  10941  supadd  12090  supmullem1  12092  uzin  12772  elfzmlbp  13539  isfinite4  14269  brfi1uzind  14415  swrdnd  14562  01sqrexlem6  15154  sqreulem  15267  fvprmselgcd1  16957  lubun  18421  lspsneq  21059  fvmptnn04ifb  22766  fbasfip  23783  alexsubALTlem2  23963  ovolunlem1  25425  dchrisum0flb  27448  nodmon  27589  noextendseq  27606  nocvxminlem  27717  brbtwn2  28883  axcontlem8  28949  isclwwlknx  30016  clwwlkel  30026  clwwlknwwlksnb  30035  wwlksext2clwwlk  30037  mdbr3  32277  mdbr4  32278  atssma  32358  atcvatlem  32365  ssrelf  32598  fnrelpredd  35102  nepss  35762  hfun  36222  bj-ax12ig  36680  bj-substw  36766  finxpreclem2  37434  indexdom  37773  fdc  37784  totbndss  37816  grpomndo  37914  iss2  38375  ax12eq  39039  ax12el  39040  lsatn0  39097  lsatcmp  39101  lsatcv0  39129  lfl1dim  39219  lfl1dim2N  39220  lkrss2N  39267  lub0N  39287  glb0N  39291  ispsubcl2N  40045  cdlemefrs29bpre0  40494  dihglblem2N  41392  dihglblem3N  41393  dochsnnz  41548  pm13.14  44501  tratrb  44628  ax6e2ndeq  44651  3impexpbicomVD  44948  tratrbVD  44952  equncomVD  44959  trsbcVD  44968  sbcssgVD  44974  csbingVD  44975  onfrALTVD  44982  csbsngVD  44984  csbxpgVD  44985  csbresgVD  44986  csbrngVD  44987  csbima12gALTVD  44988  csbunigVD  44989  csbfv12gALTVD  44990  con5VD  44991  hbimpgVD  44995  hbexgVD  44997  ax6e2ndeqVD  45000  supxrleubrnmpt  45503  suprleubrnmpt  45519  infxrgelbrnmpt  45551  usgrgrtrirex  48049  isassintop  48309  zgtp1leeq  48621