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

Theorem syl112anc 1220
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 304 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1216 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:  fvun1  5487  caseinl  6976  caseinr  6977  reapmul1  8369  recrecap  8481  rec11rap  8483  divdivdivap  8485  dmdcanap  8494  ddcanap  8498  rerecclap  8502  div2negap  8507  divap1d  8573  divmulapd  8584  apdivmuld  8585  divmulap2d  8596  divmulap3d  8597  divassapd  8598  div12apd  8599  div23apd  8600  divdirapd  8601  divsubdirapd  8602  div11apd  8603  ltmul12a  8630  ltdiv1  8638  ltrec  8653  lt2msq1  8655  lediv2  8661  lediv23  8663  recp1lt1  8669  qapne  9443  xadd4d  9680  xleaddadd  9682  modqge0  10117  modqlt  10118  modqid  10134  expgt1  10343  nnlesq  10408  expnbnd  10427  facubnd  10503  resqrexlemover  10794  mulcn2  11093  cvgratnnlemnexp  11305  cvgratnnlemmn  11306  eftlub  11408  eflegeo  11419  sin01bnd  11475  cos01bnd  11476  eirraplem  11494  bezoutlemnewy  11695  bezoutlemstep  11696  mulgcd  11715  mulgcddvds  11786  prmind2  11812  oddpwdclemxy  11858  oddpwdclemodd  11861  qnumgt0  11887  txdis  12460  txdis1cn  12461  xblm  12600  reeff1oleme  12876  tangtx  12941  cosordlem  12952  logdivlti  12979  apdifflemr  13301
  Copyright terms: Public domain W3C validator