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  2619  euan  2622  euanv  2625  eleq1a  2832  ceqsalgALT  3478  cgsexg  3486  cgsex2g  3487  cgsex4g  3488  cgsex4gOLD  3489  spcegv  3552  spc2egv  3554  reu6  3685  csbiebt  3879  dfiin2g  4987  reusv2lem2  5345  ralxfrALT  5361  axprlem4  5372  sotr3  5574  opelxp  5661  ssrel  5733  ssrel2  5735  ssrelrel  5746  iss  5995  ordun  6424  fprb  7142  riotaclb  7358  iunpw  7718  limom  7826  funcnvuni  7876  fiunlem  7888  soxp  8073  tfrlem8  8317  oaordex  8487  eroveu  8753  fundmen  8972  nneneq  9134  onfin2  9145  dif1ennnALT  9181  unfilem1  9209  rankwflemb  9709  sornom  10191  isf32lem9  10275  axdc3lem2  10365  axdc4lem  10369  zorn2lem3  10412  zorn2lem7  10416  tskuni  10698  grur1a  10734  grothomex  10744  genpnnp  10920  ltaddpr  10949  reclem4pr  10965  supadd  12114  supmullem1  12116  uzin  12791  elfzmlbp  13559  isfinite4  14289  brfi1uzind  14435  swrdnd  14582  01sqrexlem6  15174  sqreulem  15287  fvprmselgcd1  16977  lubun  18442  lspsneq  21081  fvmptnn04ifb  22799  fbasfip  23816  alexsubALTlem2  23996  ovolunlem1  25458  dchrisum0flb  27481  nodmon  27622  noextendseq  27639  nocvxminlem  27754  brbtwn2  28982  axcontlem8  29048  isclwwlknx  30115  clwwlkel  30125  clwwlknwwlksnb  30134  wwlksext2clwwlk  30136  mdbr3  32376  mdbr4  32377  atssma  32457  atcvatlem  32464  ssrelf  32696  fnrelpredd  35249  nepss  35914  hfun  36374  bj-ax12ig  36838  bj-substw  36925  finxpreclem2  37597  wl-eujustlem1  37795  indexdom  37937  fdc  37948  totbndss  37980  grpomndo  38078  iss2  38547  ax12eq  39269  ax12el  39270  lsatn0  39327  lsatcmp  39331  lsatcv0  39359  lfl1dim  39449  lfl1dim2N  39450  lkrss2N  39497  lub0N  39517  glb0N  39521  ispsubcl2N  40275  cdlemefrs29bpre0  40724  dihglblem2N  41622  dihglblem3N  41623  dochsnnz  41778  pm13.14  44717  tratrb  44844  ax6e2ndeq  44867  3impexpbicomVD  45164  tratrbVD  45168  equncomVD  45175  trsbcVD  45184  sbcssgVD  45190  csbingVD  45191  onfrALTVD  45198  csbsngVD  45200  csbxpgVD  45201  csbresgVD  45202  csbrngVD  45203  csbima12gALTVD  45204  csbunigVD  45205  csbfv12gALTVD  45206  con5VD  45207  hbimpgVD  45211  hbexgVD  45213  ax6e2ndeqVD  45216  supxrleubrnmpt  45717  suprleubrnmpt  45733  infxrgelbrnmpt  45765  usgrgrtrirex  48263  isassintop  48523  zgtp1leeq  48834