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 597. (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  2242  ax13ALT  2424  r19.30  3120  intss2  5072  vtoclr  5699  funopg  6539  abnex  7695  xpider  8733  undifixp  8878  onsdominel  9076  fodomr  9078  wemaplem2  9491  rankuni2b  9797  infxpenlem  9957  dfac8b  9975  ac10ct  9978  alephordi  10018  infdif  10153  cfflb  10203  alephval2  10516  tskxpss  10716  tskcard  10725  ingru  10759  grur1  10764  grothac  10774  suplem1pr  10996  mulgt0sr  11049  ixxssixx  13287  difelfzle  13563  swrdnd0  14554  climrlim2  15438  qshash  15720  gcdcllem3  16389  vdwlem13  16873  ocvsscon  21102  opsrtoslem2  21486  txcnp  22994  t0kq  23192  filconn  23257  filuni  23259  alexsubALTlem3  23423  rectbntr0  24218  iscau4  24666  cfilres  24683  lmcau  24700  bcthlem2  24712  subfacp1lem6  33843  cvmsdisj  33928  meran1  34936  bj-bi3ant  35107  bj-cbv3ta  35304  bj-2upleq  35533  bj-ismooredr2  35631  bj-snmoore  35634  bj-isclm  35812  relowlssretop  35884  poimirlem30  36158  poimirlem31  36159  caushft  36270  partimeq  37321  ax13fromc9  37418  harinf  41405  ntrk0kbimka  42403  onfrALTlem3  42918  onfrALTlem2  42920  e222  43010  e111  43048  e333  43107  bitr3VD  43223  disjinfi  43504  prpair  45783  onsetrec  47243  aacllem  47338
  Copyright terms: Public domain W3C validator