Theorem biimprcd 251

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  biimparc  480  ax12i  1946  moanimlem  2671  euan  2674  euanv  2678  eleq1a  2878  ceqsalgALT  3473  cgsexg  3480  cgsex2g  3481  cgsex4g  3482  ceqsex  3483  spcegv  3540  spc2egv  3542  reu6  3651  csbiebt  3837  dfiin2g  4860  reusv2lem2  5191  ralxfrALT  5207  opelxp  5479  ssrel  5543  ssrel2  5545  ssrelrel  5555  iss  5784  ordun  6167  fprb  6823  riotaclb  7015  iunpw  7349  limom  7451  funcnvuni  7492  fiunlem  7499  soxp  7676  tfrlem8  7872  oaordex  8034  eroveu  8242  fundmen  8431  nneneq  8547  onfin2  8556  dif1en  8597  unfilem1  8628  rankwflemb  9068  sornom  9545  isf32lem9  9629  axdc3lem2  9719  axdc4lem  9723  zorn2lem3  9766  zorn2lem7  9770  tskuni  10051  grur1a  10087  grothomex  10097  genpnnp  10273  ltaddpr  10302  reclem4pr  10318  supadd  11457  supmullem1  11459  uzin  12127  elfzmlbp  12868  isfinite4  13573  brfi1uzind  13702  swrdnd  13852  sqrlem6  14441  sqreulem  14553  fvprmselgcd1  16210  lubun  17562  lspsneq  19584  fvmptnn04ifb  21143  fbasfip  22160  alexsubALTlem2  22340  ovolunlem1  23781  dchrisum0flb  25768  brbtwn2  26374  axcontlem8  26440  isclwwlknx  27501  clwwlknwwlksnb  27521  mdbr3  29765  mdbr4  29766  atssma  29846  atcvatlem  29853  ssrelf  30056  nepss  32556  sotr3  32610  nodmon  32766  noextendseq  32783  nocvxminlem  32856  hfun  33248  bj-ax12ig  33571  finxpreclem2  34202  indexdom  34541  fdc  34552  totbndss  34587  grpomndo  34685  iss2  35133  ax12eq  35608  ax12el  35609  lsatn0  35666  lsatcmp  35670  lsatcv0  35698  lfl1dim  35788  lfl1dim2N  35789  lkrss2N  35836  lub0N  35856  glb0N  35860  ispsubcl2N  36614  cdlemefrs29bpre0  37063  dihglblem2N  37961  dihglblem3N  37962  dochsnnz  38117  pm13.14  40279  tratrb  40409  ax6e2ndeq  40432  3impexpbicomVD  40730  tratrbVD  40734  equncomVD  40741  trsbcVD  40750  sbcssgVD  40756  csbingVD  40757  onfrALTVD  40764  csbsngVD  40766  csbxpgVD  40767  csbresgVD  40768  csbrngVD  40769  csbima12gALTVD  40770  csbunigVD  40771  csbfv12gALTVD  40772  con5VD  40773  hbimpgVD  40777  hbexgVD  40779  ax6e2ndeqVD  40782  supxrleubrnmpt  41221  suprleubrnmpt  41238  infxrgelbrnmpt  41272  isassintop  43595  zgtp1leeq  44057