Theorem biimprcd 240

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  biimparc  504  ax12i  1879  moanim  2529  euan  2530  eleq1a  2696  ceqsalgALT  3231  cgsexg  3238  cgsex2g  3239  cgsex4g  3240  ceqsex  3241  spc2egv  3295  spc3egv  3297  reu6  3395  csbiebt  3553  dfiin2g  4553  reusv2lem2  4869  ralxfrALT  4887  opelxp  5146  ssrel  5207  ssrelOLD  5208  ssrel2  5210  ssrelrel  5220  iss  5447  ordun  5829  riotaclb  6649  iunpw  6978  limom  7080  funcnvuni  7119  fun11iun  7126  soxp  7290  tfrlem8  7480  oaordex  7638  eroveu  7842  fundmen  8030  nneneq  8143  onfin2  8152  dif1en  8193  unfilem1  8224  rankwflemb  8656  sornom  9099  isf32lem9  9183  axdc3lem2  9273  axdc4lem  9277  zorn2lem3  9320  zorn2lem7  9324  tskuni  9605  grur1a  9641  grothomex  9651  genpnnp  9827  ltaddpr  9856  reclem4pr  9872  supadd  10991  supmullem1  10993  uzin  11720  elfzmlbp  12450  isfinite4  13153  brfi1uzind  13280  brfi1uzindOLD  13286  swrdnd  13432  sqrlem6  13988  sqreulem  14099  fvprmselgcd1  15749  lubun  17123  lspsneq  19122  fvmptnn04ifb  20656  fbasfip  21672  alexsubALTlem2  21852  ovolunlem1  23265  dchrisum0flb  25199  brbtwn2  25785  axcontlem8  25851  mdbr3  29156  mdbr4  29157  atssma  29237  atcvatlem  29244  ssrelf  29425  nepss  31599  sotr3  31656  fprb  31669  frrlem4  31783  nodmon  31803  noextendseq  31820  nocvxminlem  31893  hfun  32285  bj-ax12ig  32615  finxpreclem2  33227  indexdom  33529  fdc  33541  totbndss  33576  grpomndo  33674  iss2  34112  ax12eq  34226  ax12el  34227  lsatn0  34286  lsatcmp  34290  lsatcv0  34318  lfl1dim  34408  lfl1dim2N  34409  lkrss2N  34456  lub0N  34476  glb0N  34480  ispsubcl2N  35233  cdlemefrs29bpre0  35684  dihglblem2N  36583  dihglblem3N  36584  dochsnnz  36739  pm13.14  38610  tratrb  38746  ax6e2ndeq  38775  3impexpbicomVD  39092  tratrbVD  39097  equncomVD  39104  trsbcVD  39113  sbcssgVD  39119  csbingVD  39120  onfrALTVD  39127  csbsngVD  39129  csbxpgVD  39130  csbresgVD  39131  csbrngVD  39132  csbima12gALTVD  39133  csbunigVD  39134  csbfv12gALTVD  39135  con5VD  39136  hbimpgVD  39140  hbexgVD  39142  ax6e2ndeqVD  39145  supxrleubrnmpt  39632  suprleubrnmpt  39649  infxrgelbrnmpt  39683  isassintop  41846  zgtp1leeq  42311