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

Theorem syl31anc 1252
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 )
syl31anc.5  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
Assertion
Ref Expression
syl31anc  |-  ( ph  ->  et )

Proof of Theorem syl31anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1179 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 411 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  syl32anc  1257  stoic4b  1444  enq0tr  7464  ltmul12a  8848  lt2msq1  8873  ledivp1  8891  lemul1ad  8927  lemul2ad  8928  lediv2ad  9751  xaddge0  9910  difelfznle  10167  expubnd  10611  nn0leexp2  10725  expcanlem  10730  expcand  10732  xrmaxaddlem  11303  mertenslemi1  11578  eftlub  11733  dvdsadd  11878  divalgmod  11967  gcdzeq  12058  rplpwr  12063  sqgcd  12065  bezoutr  12068  rpmulgcd2  12130  rpdvds  12134  isprm5  12177  divgcdodd  12178  oddpwdclemxy  12204  divnumden  12231  crth  12259  phimullem  12260  coprimeprodsq2  12293  pythagtriplem19  12317  pclemub  12322  pcpre1  12327  pcidlem  12358  pockthlem  12391  prmunb  12397  kerf1ghm  13230  elrhmunit  13544  xblss2ps  14381  xblss2  14382  metcnpi3  14494  limcimolemlt  14610  limccnp2cntop  14623  dvmulxxbr  14643  dvcoapbr  14648  2lgsoddprmlem1  14931  2sqlem8a  14947  2sqlem8  14948
  Copyright terms: Public domain W3C validator