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 494. (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  2158  ax13ALT  2304  vtoclr  5134  funopg  5890  xpider  7778  undifixp  7904  onsdominel  8069  fodomr  8071  wemaplem2  8412  rankuni2b  8676  infxpenlem  8796  dfac8b  8814  ac10ct  8817  alephordi  8857  infdif  8991  cfflb  9041  alephval2  9354  tskxpss  9554  tskcard  9563  ingru  9597  grur1  9602  grothac  9612  suplem1pr  9834  mulgt0sr  9886  ixxssixx  12147  difelfzle  12409  climrlim2  14228  qshash  14503  gcdcllem3  15166  vdwlem13  15640  opsrtoslem2  19425  ocvsscon  19959  txcnp  21363  t0kq  21561  filconn  21627  filuni  21629  alexsubALTlem3  21793  rectbntr0  22575  iscau4  23017  cfilres  23034  lmcau  23051  bcthlem2  23062  clwlksfoclwwlk  26863  subfacp1lem6  30928  cvmsdisj  31013  meran1  32105  bj-bi3ant  32269  bj-cbv3ta  32405  bj-2upleq  32700  relowlssretop  32882  poimirlem30  33110  poimirlem31  33111  caushft  33228  ax13fromc9  33710  harinf  37120  ntrk0kbimka  37858  onfrALTlem3  38280  onfrALTlem2  38282  e222  38382  e111  38420  e333  38481  bitr3VD  38606  onsetrec  41774  aacllem  41880
  Copyright terms: Public domain W3C validator