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  2618  euan  2621  euanv  2624  eleq1a  2830  ceqsalgALT  3502  cgsexg  3510  cgsex2g  3511  cgsex4g  3512  cgsex4gOLD  3513  ceqsexOLD  3515  spcegv  3581  spc2egv  3583  reu6  3714  csbiebt  3908  dfiin2g  5013  reusv2lem2  5374  ralxfrALT  5390  axprlem4  5401  sotr3  5607  opelxp  5695  ssrel  5766  ssrelOLD  5767  ssrel2  5769  ssrelrel  5780  iss  6027  ordun  6463  fprb  7191  riotaclb  7408  iunpw  7770  limom  7882  funcnvuni  7933  fiunlem  7945  soxp  8133  tfrlem8  8403  oaordex  8575  eroveu  8831  fundmen  9050  nneneq  9225  onfin2  9245  dif1ennnALT  9288  unfilem1  9320  rankwflemb  9812  sornom  10296  isf32lem9  10380  axdc3lem2  10470  axdc4lem  10474  zorn2lem3  10517  zorn2lem7  10521  tskuni  10802  grur1a  10838  grothomex  10848  genpnnp  11024  ltaddpr  11053  reclem4pr  11069  supadd  12215  supmullem1  12217  uzin  12897  elfzmlbp  13661  isfinite4  14385  brfi1uzind  14531  swrdnd  14677  01sqrexlem6  15271  sqreulem  15383  fvprmselgcd1  17070  lubun  18530  lspsneq  21088  fvmptnn04ifb  22794  fbasfip  23811  alexsubALTlem2  23991  ovolunlem1  25455  dchrisum0flb  27478  nodmon  27619  noextendseq  27636  nocvxminlem  27746  brbtwn2  28889  axcontlem8  28955  isclwwlknx  30022  clwwlkel  30032  clwwlknwwlksnb  30041  wwlksext2clwwlk  30043  mdbr3  32283  mdbr4  32284  atssma  32364  atcvatlem  32371  ssrelf  32600  fnrelpredd  35125  nepss  35740  hfun  36201  bj-ax12ig  36659  bj-substw  36745  finxpreclem2  37413  indexdom  37763  fdc  37774  totbndss  37806  grpomndo  37904  iss2  38367  ax12eq  38964  ax12el  38965  lsatn0  39022  lsatcmp  39026  lsatcv0  39054  lfl1dim  39144  lfl1dim2N  39145  lkrss2N  39192  lub0N  39212  glb0N  39216  ispsubcl2N  39971  cdlemefrs29bpre0  40420  dihglblem2N  41318  dihglblem3N  41319  dochsnnz  41474  pm13.14  44400  tratrb  44528  ax6e2ndeq  44551  3impexpbicomVD  44848  tratrbVD  44852  equncomVD  44859  trsbcVD  44868  sbcssgVD  44874  csbingVD  44875  onfrALTVD  44882  csbsngVD  44884  csbxpgVD  44885  csbresgVD  44886  csbrngVD  44887  csbima12gALTVD  44888  csbunigVD  44889  csbfv12gALTVD  44890  con5VD  44891  hbimpgVD  44895  hbexgVD  44897  ax6e2ndeqVD  44900  supxrleubrnmpt  45400  suprleubrnmpt  45416  infxrgelbrnmpt  45448  usgrgrtrirex  47929  isassintop  48152  zgtp1leeq  48464