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

Theorem syl112anc 1150
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 294 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1146 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  fvun1  5266  reapmul1  7659  recrecap  7759  rec11rap  7761  divdivdivap  7763  dmdcanap  7772  ddcanap  7776  rerecclap  7780  div2negap  7785  divap1d  7850  divmulapd  7861  divmulap2d  7872  divmulap3d  7873  divassapd  7874  div12apd  7875  div23apd  7876  divdirapd  7877  divsubdirapd  7878  div11apd  7879  ltmul12a  7900  ltdiv1  7908  ltrec  7923  lt2msq1  7925  lediv2  7931  lediv23  7933  recp1lt1  7939  qapne  8670  modqge0  9281  modqlt  9282  modqid  9298  expgt1  9457  nnlesq  9521  expnbnd  9539  facubnd  9612  resqrexlemover  9836  mulcn2  10063  oddpwdclemxy  10236  oddpwdclemodd  10239
  Copyright terms: Public domain W3C validator