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  1964  moanimlem  2616  euan  2619  euanv  2622  eleq1a  2834  ceqsalgALT  3516  cgsexg  3524  cgsex2g  3525  cgsex4g  3526  cgsex4gOLD  3527  ceqsexOLD  3529  ceqsexvOLD  3531  spcegv  3597  spc2egv  3599  reu6  3735  csbiebt  3938  dfiin2g  5037  reusv2lem2  5405  ralxfrALT  5421  axprlem4  5432  sotr3  5637  opelxp  5725  ssrel  5795  ssrelOLD  5796  ssrel2  5798  ssrelrel  5809  iss  6055  ordun  6490  fprb  7214  riotaclb  7429  iunpw  7790  limom  7903  funcnvuni  7955  fiunlem  7965  soxp  8153  tfrlem8  8423  oaordex  8595  eroveu  8851  fundmen  9070  nneneq  9244  nneneqOLD  9256  onfin2  9266  dif1ennnALT  9309  unfilem1  9341  rankwflemb  9831  sornom  10315  isf32lem9  10399  axdc3lem2  10489  axdc4lem  10493  zorn2lem3  10536  zorn2lem7  10540  tskuni  10821  grur1a  10857  grothomex  10867  genpnnp  11043  ltaddpr  11072  reclem4pr  11088  supadd  12234  supmullem1  12236  uzin  12916  elfzmlbp  13676  isfinite4  14398  brfi1uzind  14544  swrdnd  14689  01sqrexlem6  15283  sqreulem  15395  fvprmselgcd1  17079  lubun  18573  lspsneq  21142  fvmptnn04ifb  22873  fbasfip  23892  alexsubALTlem2  24072  ovolunlem1  25546  dchrisum0flb  27569  nodmon  27710  noextendseq  27727  nocvxminlem  27837  brbtwn2  28935  axcontlem8  29001  isclwwlknx  30065  clwwlkel  30075  clwwlknwwlksnb  30084  wwlksext2clwwlk  30086  mdbr3  32326  mdbr4  32327  atssma  32407  atcvatlem  32414  ssrelf  32635  fnrelpredd  35082  nepss  35698  hfun  36160  bj-ax12ig  36619  bj-substw  36705  finxpreclem2  37373  indexdom  37721  fdc  37732  totbndss  37764  grpomndo  37862  iss2  38326  ax12eq  38923  ax12el  38924  lsatn0  38981  lsatcmp  38985  lsatcv0  39013  lfl1dim  39103  lfl1dim2N  39104  lkrss2N  39151  lub0N  39171  glb0N  39175  ispsubcl2N  39930  cdlemefrs29bpre0  40379  dihglblem2N  41277  dihglblem3N  41278  dochsnnz  41433  pm13.14  44405  tratrb  44534  ax6e2ndeq  44557  3impexpbicomVD  44855  tratrbVD  44859  equncomVD  44866  trsbcVD  44875  sbcssgVD  44881  csbingVD  44882  onfrALTVD  44889  csbsngVD  44891  csbxpgVD  44892  csbresgVD  44893  csbrngVD  44894  csbima12gALTVD  44895  csbunigVD  44896  csbfv12gALTVD  44897  con5VD  44898  hbimpgVD  44902  hbexgVD  44904  ax6e2ndeqVD  44907  supxrleubrnmpt  45356  suprleubrnmpt  45372  infxrgelbrnmpt  45404  usgrgrtrirex  47853  isassintop  48054  zgtp1leeq  48367