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

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

Proof of Theorem syl112anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
53, 4jca 300 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1170 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  fvun1  5313  reapmul1  7970  recrecap  8072  rec11rap  8074  divdivdivap  8076  dmdcanap  8085  ddcanap  8089  rerecclap  8093  div2negap  8098  divap1d  8163  divmulapd  8174  divmulap2d  8185  divmulap3d  8186  divassapd  8187  div12apd  8188  div23apd  8189  divdirapd  8190  divsubdirapd  8191  div11apd  8192  ltmul12a  8213  ltdiv1  8221  ltrec  8236  lt2msq1  8238  lediv2  8244  lediv23  8246  recp1lt1  8252  qapne  9017  modqge0  9626  modqlt  9627  modqid  9643  expgt1  9828  nnlesq  9892  expnbnd  9910  facubnd  9986  resqrexlemover  10268  mulcn2  10523  bezoutlemnewy  10763  bezoutlemstep  10764  mulgcd  10783  mulgcddvds  10854  prmind2  10880  oddpwdclemxy  10925  oddpwdclemodd  10928  qnumgt0  10954
  Copyright terms: Public domain W3C validator