Theorem biimprcd 249

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 246	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimparc  480  ax12i  1970  moanimlem  2614  euan  2617  euanv  2620  eleq1a  2828  ceqsalgALT  3508  cgsexg  3518  cgsex2g  3519  cgsex4g  3520  cgsex4gOLD  3521  cgsex4gOLDOLD  3522  ceqsexOLD  3524  ceqsexvOLD  3526  spcegv  3587  spc2egv  3589  reu6  3721  csbiebt  3922  dfiin2g  5034  reusv2lem2  5396  ralxfrALT  5412  sotr3  5626  opelxp  5711  ssrel  5780  ssrelOLD  5781  ssrel2  5783  ssrelrel  5794  iss  6033  ordun  6465  fprb  7191  riotaclb  7403  iunpw  7754  limom  7867  funcnvuni  7918  fiunlem  7924  soxp  8111  tfrlem8  8380  oaordex  8554  eroveu  8802  fundmen  9027  nneneq  9205  nneneqOLD  9217  onfin2  9227  dif1ennnALT  9273  unfilem1  9306  rankwflemb  9784  sornom  10268  isf32lem9  10352  axdc3lem2  10442  axdc4lem  10446  zorn2lem3  10489  zorn2lem7  10493  tskuni  10774  grur1a  10810  grothomex  10820  genpnnp  10996  ltaddpr  11025  reclem4pr  11041  supadd  12178  supmullem1  12180  uzin  12858  elfzmlbp  13608  isfinite4  14318  brfi1uzind  14455  swrdnd  14600  01sqrexlem6  15190  sqreulem  15302  fvprmselgcd1  16974  lubun  18464  lspsneq  20727  fvmptnn04ifb  22344  fbasfip  23363  alexsubALTlem2  23543  ovolunlem1  25005  dchrisum0flb  27002  nodmon  27142  noextendseq  27159  nocvxminlem  27268  brbtwn2  28152  axcontlem8  28218  isclwwlknx  29278  clwwlkel  29288  clwwlknwwlksnb  29297  wwlksext2clwwlk  29299  mdbr3  31537  mdbr4  31538  atssma  31618  atcvatlem  31625  ssrelf  31831  fnrelpredd  34080  nepss  34675  hfun  35138  bj-ax12ig  35501  bj-substw  35588  finxpreclem2  36259  indexdom  36590  fdc  36601  totbndss  36633  grpomndo  36731  iss2  37201  ax12eq  37799  ax12el  37800  lsatn0  37857  lsatcmp  37861  lsatcv0  37889  lfl1dim  37979  lfl1dim2N  37980  lkrss2N  38027  lub0N  38047  glb0N  38051  ispsubcl2N  38806  cdlemefrs29bpre0  39255  dihglblem2N  40153  dihglblem3N  40154  dochsnnz  40309  pm13.14  43153  tratrb  43282  ax6e2ndeq  43305  3impexpbicomVD  43603  tratrbVD  43607  equncomVD  43614  trsbcVD  43623  sbcssgVD  43629  csbingVD  43630  onfrALTVD  43637  csbsngVD  43639  csbxpgVD  43640  csbresgVD  43641  csbrngVD  43642  csbima12gALTVD  43643  csbunigVD  43644  csbfv12gALTVD  43645  con5VD  43646  hbimpgVD  43650  hbexgVD  43652  ax6e2ndeqVD  43655  supxrleubrnmpt  44102  suprleubrnmpt  44118  infxrgelbrnmpt  44150  isassintop  46606  zgtp1leeq  47155