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

Theorem syl13anc 1218
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 1161 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 408 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  syl23anc  1223  syl33anc  1231  caovassd  5930  caovcand  5933  caovordid  5937  caovordd  5939  caovdid  5946  caovdird  5949  swoer  6457  swoord1  6458  swoord2  6459  fimax2gtrilemstep  6794  iunfidisj  6834  ssfii  6862  suplub2ti  6888  prarloclem3  7317  fzosubel3  9985  seq3split  10264  seq3caopr  10268  zsumdc  11165  fsumiun  11258  divalglemex  11630  strle1g  12063  psmetsym  12512  psmettri  12513  psmetge0  12514  psmetres2  12516  xmetge0  12548  xmetsym  12551  xmettri  12555  metrtri  12560  xmetres2  12562  bldisj  12584  xblss2ps  12587  xblss2  12588  xmeter  12619  xmetxp  12690
  Copyright terms: Public domain W3C validator