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 575. (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  axc16gOLD  2323  ax13ALT  2460  vtoclr  5304  funopg  6065  abnex  7111  xpider  7969  undifixp  8097  onsdominel  8264  fodomr  8266  wemaplem2  8607  rankuni2b  8879  infxpenlem  9035  dfac8b  9053  ac10ct  9056  alephordi  9096  infdif  9232  cfflb  9282  alephval2  9595  tskxpss  9795  tskcard  9804  ingru  9838  grur1  9843  grothac  9853  suplem1pr  10075  mulgt0sr  10127  ixxssixx  12393  difelfzle  12659  climrlim2  14485  qshash  14765  gcdcllem3  15430  vdwlem13  15903  opsrtoslem2  19699  ocvsscon  20235  txcnp  21643  t0kq  21841  filconn  21906  filuni  21908  alexsubALTlem3  22072  rectbntr0  22854  iscau4  23295  cfilres  23312  lmcau  23329  bcthlem2  23340  clwlksfoclwwlkOLD  27241  subfacp1lem6  31499  cvmsdisj  31584  meran1  32741  bj-bi3ant  32905  bj-cbv3ta  33041  bj-2upleq  33325  bj-intss  33378  bj-snmoore  33393  relowlssretop  33541  poimirlem30  33765  poimirlem31  33766  caushft  33882  ax13fromc9  34707  harinf  38120  ntrk0kbimka  38856  onfrALTlem3  39278  onfrALTlem2  39280  e222  39380  e111  39418  e333  39479  bitr3VD  39600  onsetrec  42972  aacllem  43068
  Copyright terms: Public domain W3C validator