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  1966  moanimlem  2611  euan  2614  euanv  2617  eleq1a  2823  ceqsalgALT  3481  cgsexg  3489  cgsex2g  3490  cgsex4g  3491  cgsex4gOLD  3492  ceqsexOLD  3494  spcegv  3560  spc2egv  3562  reu6  3694  csbiebt  3888  dfiin2g  4991  reusv2lem2  5349  ralxfrALT  5365  axprlem4  5376  sotr3  5580  opelxp  5667  ssrel  5737  ssrel2  5739  ssrelrel  5750  iss  5995  ordun  6426  fprb  7150  riotaclb  7367  iunpw  7727  limom  7838  funcnvuni  7888  fiunlem  7900  soxp  8085  tfrlem8  8329  oaordex  8499  eroveu  8762  fundmen  8979  nneneq  9147  onfin2  9157  dif1ennnALT  9198  unfilem1  9230  rankwflemb  9724  sornom  10208  isf32lem9  10292  axdc3lem2  10382  axdc4lem  10386  zorn2lem3  10429  zorn2lem7  10433  tskuni  10714  grur1a  10750  grothomex  10760  genpnnp  10936  ltaddpr  10965  reclem4pr  10981  supadd  12129  supmullem1  12131  uzin  12811  elfzmlbp  13578  isfinite4  14305  brfi1uzind  14451  swrdnd  14597  01sqrexlem6  15190  sqreulem  15303  fvprmselgcd1  16993  lubun  18457  lspsneq  21065  fvmptnn04ifb  22772  fbasfip  23789  alexsubALTlem2  23969  ovolunlem1  25432  dchrisum0flb  27455  nodmon  27596  noextendseq  27613  nocvxminlem  27724  brbtwn2  28886  axcontlem8  28952  isclwwlknx  30016  clwwlkel  30026  clwwlknwwlksnb  30035  wwlksext2clwwlk  30037  mdbr3  32277  mdbr4  32278  atssma  32358  atcvatlem  32365  ssrelf  32594  fnrelpredd  35073  nepss  35699  hfun  36160  bj-ax12ig  36618  bj-substw  36704  finxpreclem2  37372  indexdom  37722  fdc  37733  totbndss  37765  grpomndo  37863  iss2  38320  ax12eq  38928  ax12el  38929  lsatn0  38986  lsatcmp  38990  lsatcv0  39018  lfl1dim  39108  lfl1dim2N  39109  lkrss2N  39156  lub0N  39176  glb0N  39180  ispsubcl2N  39935  cdlemefrs29bpre0  40384  dihglblem2N  41282  dihglblem3N  41283  dochsnnz  41438  pm13.14  44392  tratrb  44520  ax6e2ndeq  44543  3impexpbicomVD  44840  tratrbVD  44844  equncomVD  44851  trsbcVD  44860  sbcssgVD  44866  csbingVD  44867  onfrALTVD  44874  csbsngVD  44876  csbxpgVD  44877  csbresgVD  44878  csbrngVD  44879  csbima12gALTVD  44880  csbunigVD  44881  csbfv12gALTVD  44882  con5VD  44883  hbimpgVD  44887  hbexgVD  44889  ax6e2ndeqVD  44892  supxrleubrnmpt  45396  suprleubrnmpt  45412  infxrgelbrnmpt  45444  usgrgrtrirex  47943  isassintop  48192  zgtp1leeq  48504