ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl13anc Unicode version

Theorem syl13anc 1183
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
syl13anc.5  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
Assertion
Ref Expression
syl13anc  |-  ( ph  ->  et )

Proof of Theorem syl13anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
52, 3, 43jca 1126 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 404 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 929
This theorem is referenced by:  syl23anc  1188  syl33anc  1196  caovassd  5842  caovcand  5845  caovordid  5849  caovordd  5851  caovdid  5858  caovdird  5861  swoer  6360  swoord1  6361  swoord2  6362  fimax2gtrilemstep  6696  iunfidisj  6735  suplub2ti  6776  prarloclem3  7153  fzosubel3  9756  seq3split  10045  seq3caopr  10049  zsumdc  10943  fsumiun  11036  divalglemex  11365  strle1g  11749  psmetsym  12131  psmettri  12132  psmetge0  12133  psmetres2  12135  xmetge0  12167  xmetsym  12170  xmettri  12174  metrtri  12179  xmetres2  12181  bldisj  12203  xblss2ps  12206  xblss2  12207  xmeter  12238
  Copyright terms: Public domain W3C validator