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  7184  cflim2  7889  axpre-sup  8791  xle2add  10579  fzen  10811  rpmulgcd2  12784  pcqmul  12906  plttr  14104  pospo  14107  lubid  14116  latjlej12  14173  latmlem12  14189  cygabl  15177  hausnei2  17081  uncmp  17130  itgsubst  19396  dvdsmulf1o  20434  2sqlem8a  20610  shintcli  21908  cvntr  22872  cdj3i  23021  axcontlem9  24600  toplat  25290  cmpmon  25815  dihmeetlem1N  31480
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