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  7892  cflim2  8644  axpre-sup  9547  xle2add  11452  fzen  11704  rpmulgcd2  14108  pcqmul  14239  plttr  15460  pospo  15463  lublecllem  15478  latjlej12  15557  latmlem12  15573  cygabl  16708  hausnei2  19660  uncmp  19709  itgsubst  22277  dvdsmulf1o  23295  2sqlem8a  23471  axcontlem9  24048  usg2wotspth  24657  numclwlk1lem2f1  24868  shintcli  26020  cvntr  26984  cdj3i  27133  heicant  29902  itg2addnc  29922  bj-bary1  33970  dihmeetlem1N  36304
  Copyright terms: Public domain W3C validator