MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2im Structured version   Visualization version   GIF version

Theorem syl2im 40
Description: Replace two antecedents. Implication-only version of syl2an 598. (Contributed by Wolf Lammen, 14-May-2013.)
Hypotheses
Ref Expression
syl2im.1 (𝜑𝜓)
syl2im.2 (𝜒𝜃)
syl2im.3 (𝜓 → (𝜃𝜏))
Assertion
Ref Expression
syl2im (𝜑 → (𝜒𝜏))

Proof of Theorem syl2im
StepHypRef Expression
1 syl2im.1 . 2 (𝜑𝜓)
2 syl2im.2 . . 3 (𝜒𝜃)
3 syl2im.3 . . 3 (𝜓 → (𝜃𝜏))
42, 3syl5 34 . 2 (𝜓 → (𝜒𝜏))
51, 4syl 17 1 (𝜑 → (𝜒𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl2imc  41  sylc  65  sbequ2  2252  ax13ALT  2449  vtoclr  5602  funopg  6377  abnex  7469  xpider  8358  undifixp  8488  onsdominel  8657  fodomr  8659  wemaplem2  9002  rankuni2b  9273  infxpenlem  9431  dfac8b  9449  ac10ct  9452  alephordi  9492  infdif  9623  cfflb  9673  alephval2  9986  tskxpss  10186  tskcard  10195  ingru  10229  grur1  10234  grothac  10244  suplem1pr  10466  mulgt0sr  10519  ixxssixx  12745  difelfzle  13020  swrdnd0  14015  climrlim2  14900  qshash  15178  gcdcllem3  15844  vdwlem13  16323  opsrtoslem2  20258  ocvsscon  20812  txcnp  22221  t0kq  22419  filconn  22484  filuni  22486  alexsubALTlem3  22650  rectbntr0  23433  iscau4  23879  cfilres  23896  lmcau  23913  bcthlem2  23925  subfacp1lem6  32457  cvmsdisj  32542  meran1  33784  bj-bi3ant  33948  bj-cbv3ta  34135  bj-2upleq  34360  bj-intss  34427  bj-ismooredr2  34438  bj-snmoore  34441  bj-isclm  34618  relowlssretop  34692  poimirlem30  34997  poimirlem31  34998  caushft  35109  ax13fromc9  36112  harinf  39828  ntrk0kbimka  40598  onfrALTlem3  41107  onfrALTlem2  41109  e222  41199  e111  41237  e333  41296  bitr3VD  41412  disjinfi  41682  prpair  43881  onsetrec  45088  aacllem  45180
  Copyright terms: Public domain W3C validator