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

Theorem syl2and 471
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 470 . 2  |-  ( ph  ->  ( ( ch  /\  th )  ->  et )
)
51, 4syland 469 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  et )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  anim12d  548  dffi3  7438  cflim2  8145  axpre-sup  9046  xle2add  10840  fzen  11074  rpmulgcd2  13107  pcqmul  13229  plttr  14429  pospo  14432  lubid  14441  latjlej12  14498  latmlem12  14514  cygabl  15502  hausnei2  17419  uncmp  17468  itgsubst  19935  dvdsmulf1o  20981  2sqlem8a  21157  shintcli  22833  cvntr  23797  cdj3i  23946  axcontlem9  25913  itg2addnc  26261  usg2wotspth  28404  dihmeetlem1N  32150
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 179  df-an 362
  Copyright terms: Public domain W3C validator