Theorem biimprcd 253

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 23	. 2 ⊢ (𝜒 → 𝜒)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibrcom 250	1 ⊢ (𝜒 → (𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimparc  485  ax12i  2001  moanimlem  2646  euan  2649  euanv  2652  eleq1a  2859  ceqsalgALT  3490  cgsexg  3498  cgsex2g  3499  cgsex4g  3500  spcegv  3555  spc2egv  3557  reu6  3687  csbiebt  3880  reusv2lem2  5365  ralxfrALT  5381  axprlem4  5392  sotr3  5604  opelxp  5691  ssrel  5764  ssrel2  5766  ssrelrel  5777  iss  6038  ordun  6484  fprb  7219  riotaclb  7438  iunpw  7806  limom  7914  funcnvuni  7965  fiunlem  7975  soxp  8165  tfrlem8  8417  oaordex  8591  eroveu  8858  fundmen  9084  nneneq  9246  onfin2  9257  dif1ennnALT  9293  unfilem1  9322  elirrv  9615  rankwflemb  9824  rankwflembOLD  9825  hfunOLD  9943  sornom  10379  isf32lem9  10463  axdc3lem2  10553  axdc4lem  10557  zorn2lem3  10600  zorn2lem7  10604  tskuni  10892  grur1a  10928  grothomex  10938  genpnnp  11114  ltaddpr  11143  reclem4pr  11159  supadd  12309  supmullem1  12311  uzin  13025  elfzmlbp  13797  isfinite4  14530  brfi1uzind  14677  swrdnd  14829  01sqrexlem6  15440  sqreulem  15553  fvprmselgcd1  17249  lubun  18715  lspsneq  21427  fvmptnn04ifb  23196  fbasfip  24214  alexsubALTlem2  24394  ovolunlem1  25845  dchrisum0flb  27864  nodmon  28034  noextendseq  28051  nocvxminlem  28167  brbtwn2  29510  axcontlem8  29576  isclwwlknx  30654  clwwlkel  30664  clwwlknwwlksnb  30673  wwlksext2clwwlk  30675  mdbr3  32926  mdbr4  32927  atssma  33007  atcvatlem  33014  ssrelf  33278  reu6f  35776  fnrelpredd  35801  jf1o  36010  elpssmo  36635  nepss  36660  nmulprop  37116  axtco2  37439  axtcond  37443  bj-ax12ig  37697  bj-alextruim  37713  bj-substw  37804  bj-axreprepsep  38181  finxpreclem2  38504  wl-eujustlem1  38711  indexdom  38859  fdc  38870  totbndss  38902  grpomndo  39000  iss2  39467  ax12eq  40189  ax12el  40190  lsatn0  40247  lsatcmp  40251  lsatcv0  40279  lfl1dim  40369  lfl1dim2N  40370  lkrss2N  40417  lub0N  40437  glb0N  40441  ispsubcl2N  41195  cdlemefrs29bpre0  41644  dihglblem2N  42542  dihglblem3N  42543  dochsnnz  42698  pm13.14  45583  tratrb  45708  ax6e2ndeq  45731  3impexpbicomVD  46028  tratrbVD  46032  equncomVD  46039  trsbcVD  46048  sbcssgVD  46054  csbingVD  46055  onfrALTVD  46062  csbsngVD  46064  csbxpgVD  46065  csbresgVD  46066  csbrngVD  46067  csbima12gALTVD  46068  csbunigVD  46069  csbfv12gALTVD  46070  con5VD  46071  hbimpgVD  46075  hbexgVD  46077  ax6e2ndeqVD  46080  supxrleubrnmpt  46619  suprleubrnmpt  46635  infxrgelbrnmpt  46667  usgrgrtrirex  49251  isassintop  49510  zgtp1leeq  49836