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 594. (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  2236  ax13ALT  2418  r19.30  3109  intss2  5112  vtoclr  5741  funopg  6588  feldmfvelcdm  7095  abnex  7760  xpider  8807  undifixp  8953  onsdominel  9154  fodomr  9156  wemaplem2  9577  rankuni2b  9883  infxpenlem  10043  dfac8b  10061  ac10ct  10064  alephordi  10104  infdif  10239  cfflb  10289  alephval2  10602  tskxpss  10802  tskcard  10811  ingru  10845  grur1  10850  grothac  10860  suplem1pr  11082  mulgt0sr  11135  ixxssixx  13378  difelfzle  13654  swrdnd0  14651  climrlim2  15535  qshash  15817  gcdcllem3  16487  vdwlem13  16981  ocvsscon  21641  opsrtoslem2  22039  txcnp  23585  t0kq  23783  filconn  23848  filuni  23850  alexsubALTlem3  24014  rectbntr0  24809  iscau4  25268  cfilres  25285  lmcau  25302  bcthlem2  25314  subfacp1lem6  34946  cvmsdisj  35031  meran1  36046  bj-bi3ant  36217  bj-cbv3ta  36414  bj-2upleq  36642  bj-ismooredr2  36740  bj-snmoore  36743  bj-isclm  36921  relowlssretop  36993  poimirlem30  37274  poimirlem31  37275  caushft  37385  partimeq  38431  ax13fromc9  38528  harinf  42602  ntrk0kbimka  43616  onfrALTlem3  44130  onfrALTlem2  44132  e222  44222  e111  44260  e333  44319  bitr3VD  44435  disjinfi  44709  prpair  46983  onsetrec  48330  aacllem  48425
  Copyright terms: Public domain W3C validator