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

Theorem syl2and 469
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 468 . 2  |-  ( ph  ->  ( ( ch  /\  th )  ->  et )
)
51, 4syland 467 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  et )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anim12d  546  dffi3  7200  cflim2  7905  axpre-sup  8807  xle2add  10595  fzen  10827  rpmulgcd2  12800  pcqmul  12922  plttr  14120  pospo  14123  lubid  14132  latjlej12  14189  latmlem12  14205  cygabl  15193  hausnei2  17097  uncmp  17146  itgsubst  19412  dvdsmulf1o  20450  2sqlem8a  20626  shintcli  21924  cvntr  22888  cdj3i  23037  axcontlem9  24672  toplat  25393  cmpmon  25918  dihmeetlem1N  32102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator