MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2and Structured version   Unicode version

Theorem syl2and 483
Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
Hypotheses
Ref Expression
syl2and.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl2and.2  |-  ( ph  ->  ( th  ->  ta ) )
syl2and.3  |-  ( ph  ->  ( ( ch  /\  ta )  ->  et ) )
Assertion
Ref Expression
syl2and  |-  ( ph  ->  ( ( ps  /\  th )  ->  et )
)

Proof of Theorem syl2and
StepHypRef Expression
1 syl2and.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl2and.2 . . 3  |-  ( ph  ->  ( th  ->  ta ) )
3 syl2and.3 . . 3  |-  ( ph  ->  ( ( ch  /\  ta )  ->  et ) )
42, 3sylan2d 482 . 2  |-  ( ph  ->  ( ( ch  /\  th )  ->  et )
)
51, 4syland 481 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  et )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  anim12d  563  dffi3  7681  cflim2  8432  axpre-sup  9336  xle2add  11222  fzen  11467  rpmulgcd2  13791  pcqmul  13920  plttr  15140  pospo  15143  lublecllem  15158  latjlej12  15237  latmlem12  15253  cygabl  16367  hausnei2  18957  uncmp  19006  itgsubst  21521  dvdsmulf1o  22534  2sqlem8a  22710  axcontlem9  23218  shintcli  24732  cvntr  25696  cdj3i  25845  heicant  28426  itg2addnc  28446  usg2wotspth  30403  numclwlk1lem2f1  30687  bj-bary1  32601  dihmeetlem1N  34935
  Copyright terms: Public domain W3C validator