Theorem syl112anc 1254

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

Step	Hyp	Ref	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 )
5	3, 4	jca 306	. 2 |- ( ph -> ( th /\ ta ) )
6		syl112anc.5	. 2 |- ( ( ps /\ ch /\ ( th /\ ta ) ) -> et )
7	1, 2, 5, 6	syl3anc 1250	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

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 983

This theorem is referenced by:  fvun1  5645  caseinl  7193  caseinr  7194  reapmul1  8668  recrecap  8782  rec11rap  8784  divdivdivap  8786  dmdcanap  8795  ddcanap  8799  rerecclap  8803  div2negap  8808  divap1d  8874  divmulapd  8885  apdivmuld  8886  divmulap2d  8897  divmulap3d  8898  divassapd  8899  div12apd  8900  div23apd  8901  divdirapd  8902  divsubdirapd  8903  div11apd  8904  ltmul12a  8933  ltdiv1  8941  ltrec  8956  lt2msq1  8958  lediv2  8964  lediv23  8966  recp1lt1  8972  qapne  9760  xadd4d  10007  xleaddadd  10009  modqge0  10477  modqlt  10478  modqid  10494  expgt1  10722  nnlesq  10788  expnbnd  10808  facubnd  10890  resqrexlemover  11321  mulcn2  11623  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  eftlub  12001  eflegeo  12012  sin01bnd  12068  cos01bnd  12069  eirraplem  12088  bitsmod  12267  bezoutlemnewy  12317  bezoutlemstep  12318  mulgcd  12337  mulgcddvds  12416  prmind2  12442  oddpwdclemxy  12491  oddpwdclemodd  12494  qnumgt0  12520  pcpremul  12616  fldivp1  12671  pcfaclem  12672  qexpz  12675  prmpwdvds  12678  pockthg  12680  4sqlem10  12710  4sqlem12  12725  4sqlem16  12729  4sqlem17  12730  ablsub4  13649  znrrg  14422  txdis  14749  txdis1cn  14750  xblm  14889  reeff1oleme  15244  tangtx  15310  cosordlem  15321  logdivlti  15353  apcxp2  15411  mersenne  15469  lgsdilem  15504  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgsquadlem1  15554  lgsquadlem2  15555  2sqlem3  15594  2sqlem8  15600  apdifflemr  15986