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  484  ax12i  1995  moanimlem  2645  euan  2648  euanv  2651  eleq1a  2857  ceqsalgALT  3490  cgsexg  3498  cgsex2g  3499  cgsex4g  3500  spcegv  3555  spc2egv  3557  reu6  3688  csbiebt  3881  reusv2lem2  5369  ralxfrALT  5385  axprlem4  5396  sotr3  5609  opelxp  5696  ssrel  5768  ssrel2  5770  ssrelrel  5781  iss  6036  ordun  6467  fprb  7192  riotaclb  7410  iunpw  7768  limom  7876  funcnvuni  7927  fiunlem  7937  soxp  8123  tfrlem8  8369  oaordex  8541  eroveu  8808  fundmen  9026  nneneq  9188  onfin2  9199  dif1ennnALT  9235  unfilem1  9263  elirrv  9557  rankwflemb  9763  sornom  10267  isf32lem9  10351  axdc3lem2  10441  axdc4lem  10445  zorn2lem3  10488  zorn2lem7  10492  tskuni  10774  grur1a  10810  grothomex  10820  genpnnp  10996  ltaddpr  11025  reclem4pr  11041  supadd  12189  supmullem1  12191  uzin  12904  elfzmlbp  13674  isfinite4  14405  brfi1uzind  14552  swrdnd  14699  01sqrexlem6  15305  sqreulem  15418  fvprmselgcd1  17111  lubun  18577  lspsneq  21257  fvmptnn04ifb  23019  fbasfip  24036  alexsubALTlem2  24216  ovolunlem1  25667  dchrisum0flb  27685  nodmon  27825  noextendseq  27842  nocvxminlem  27958  brbtwn2  29266  axcontlem8  29332  isclwwlknx  30398  clwwlkel  30408  clwwlknwwlksnb  30417  wwlksext2clwwlk  30419  mdbr3  32660  mdbr4  32661  atssma  32741  atcvatlem  32748  ssrelf  32971  fnrelpredd  35491  nepss  36218  hfun  36678  nmulprop  36690  axtco2  37013  axtcond  37017  bj-ax12ig  37271  bj-alextruim  37287  bj-substw  37378  bj-axreprepsep  37740  finxpreclem2  38064  wl-eujustlem1  38271  indexdom  38413  fdc  38424  totbndss  38456  grpomndo  38554  iss2  39021  ax12eq  39743  ax12el  39744  lsatn0  39801  lsatcmp  39805  lsatcv0  39833  lfl1dim  39923  lfl1dim2N  39924  lkrss2N  39971  lub0N  39991  glb0N  39995  ispsubcl2N  40749  cdlemefrs29bpre0  41198  dihglblem2N  42096  dihglblem3N  42097  dochsnnz  42252  pm13.14  45147  tratrb  45273  ax6e2ndeq  45296  3impexpbicomVD  45593  tratrbVD  45597  equncomVD  45604  trsbcVD  45613  sbcssgVD  45619  csbingVD  45620  onfrALTVD  45627  csbsngVD  45629  csbxpgVD  45630  csbresgVD  45631  csbrngVD  45632  csbima12gALTVD  45633  csbunigVD  45634  csbfv12gALTVD  45635  con5VD  45636  hbimpgVD  45640  hbexgVD  45642  ax6e2ndeqVD  45645  supxrleubrnmpt  46148  suprleubrnmpt  46164  infxrgelbrnmpt  46196  usgrgrtrirex  48743  isassintop  49003  zgtp1leeq  49329