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

Theorem syl2and 486
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 485 . 2  |-  ( ph  ->  ( ( ch  /\  th )  ->  et )
)
51, 4syland 484 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  et )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  anim12d  566  ax7  1860  dffi3  7945  cflim2  8693  axpre-sup  9593  xle2add  11545  fzen  11816  rpmulgcd2  14662  pcqmul  14803  initoeu1  15906  termoeu1  15913  plttr  16216  pospo  16219  lublecllem  16234  latjlej12  16313  latmlem12  16329  cygabl  17525  hausnei2  20369  uncmp  20418  itgsubst  23001  dvdsmulf1o  24123  2sqlem8a  24299  axcontlem9  25002  usg2wotspth  25612  numclwlk1lem2f1  25822  shintcli  26982  cvntr  27945  cdj3i  28094  bj-bary1  31717  heicant  31975  itg2addnc  31996  dihmeetlem1N  34858
  Copyright terms: Public domain W3C validator