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

Theorem syl2and 485
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 484 . 2  |-  ( ph  ->  ( ( ch  /\  th )  ->  et )
)
51, 4syland 483 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  et )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  anim12d  565  dffi3  7942  cflim2  8682  axpre-sup  9582  xle2add  11534  fzen  11803  rpmulgcd2  14622  pcqmul  14755  initoeu1  15850  termoeu1  15857  plttr  16160  pospo  16163  lublecllem  16178  latjlej12  16257  latmlem12  16273  cygabl  17453  hausnei2  20293  uncmp  20342  itgsubst  22895  dvdsmulf1o  24012  2sqlem8a  24188  axcontlem9  24874  usg2wotspth  25483  numclwlk1lem2f1  25693  shintcli  26843  cvntr  27806  cdj3i  27955  bj-bary1  31488  heicant  31708  itg2addnc  31729  dihmeetlem1N  34596
  Copyright terms: Public domain W3C validator