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  2618  euan  2621  euanv  2624  eleq1a  2831  ceqsalgALT  3466  cgsexg  3474  cgsex2g  3475  cgsex4g  3476  spcegv  3539  spc2egv  3541  reu6  3672  csbiebt  3866  reusv2lem2  5341  ralxfrALT  5357  axprlem4  5368  sotr3  5580  opelxp  5667  ssrel  5739  ssrel2  5741  ssrelrel  5752  iss  6000  ordun  6429  fprb  7149  riotaclb  7365  iunpw  7725  limom  7833  funcnvuni  7883  fiunlem  7895  soxp  8079  tfrlem8  8323  oaordex  8493  eroveu  8759  fundmen  8978  nneneq  9140  onfin2  9151  dif1ennnALT  9187  unfilem1  9215  rankwflemb  9717  sornom  10199  isf32lem9  10283  axdc3lem2  10373  axdc4lem  10377  zorn2lem3  10420  zorn2lem7  10424  tskuni  10706  grur1a  10742  grothomex  10752  genpnnp  10928  ltaddpr  10957  reclem4pr  10973  supadd  12124  supmullem1  12126  uzin  12824  elfzmlbp  13593  isfinite4  14324  brfi1uzind  14470  swrdnd  14617  01sqrexlem6  15209  sqreulem  15322  fvprmselgcd1  17016  lubun  18481  lspsneq  21120  fvmptnn04ifb  22816  fbasfip  23833  alexsubALTlem2  24013  ovolunlem1  25464  dchrisum0flb  27473  nodmon  27614  noextendseq  27631  nocvxminlem  27746  brbtwn2  28974  axcontlem8  29040  isclwwlknx  30106  clwwlkel  30116  clwwlknwwlksnb  30125  wwlksext2clwwlk  30127  mdbr3  32368  mdbr4  32369  atssma  32449  atcvatlem  32456  ssrelf  32688  fnrelpredd  35234  nepss  35900  hfun  36360  axtco2  36656  axtcond  36660  bj-ax12ig  36915  bj-alextruim  36931  bj-substw  37022  bj-axreprepsep  37382  finxpreclem2  37706  wl-eujustlem1  37913  indexdom  38055  fdc  38066  totbndss  38098  grpomndo  38196  iss2  38665  ax12eq  39387  ax12el  39388  lsatn0  39445  lsatcmp  39449  lsatcv0  39477  lfl1dim  39567  lfl1dim2N  39568  lkrss2N  39615  lub0N  39635  glb0N  39639  ispsubcl2N  40393  cdlemefrs29bpre0  40842  dihglblem2N  41740  dihglblem3N  41741  dochsnnz  41896  pm13.14  44836  tratrb  44963  ax6e2ndeq  44986  3impexpbicomVD  45283  tratrbVD  45287  equncomVD  45294  trsbcVD  45303  sbcssgVD  45309  csbingVD  45310  onfrALTVD  45317  csbsngVD  45319  csbxpgVD  45320  csbresgVD  45321  csbrngVD  45322  csbima12gALTVD  45323  csbunigVD  45324  csbfv12gALTVD  45325  con5VD  45326  hbimpgVD  45330  hbexgVD  45332  ax6e2ndeqVD  45335  supxrleubrnmpt  45834  suprleubrnmpt  45850  infxrgelbrnmpt  45882  usgrgrtrirex  48426  isassintop  48686  zgtp1leeq  48997