Theorem syl112anc 1277

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 1273	1 |- ( ph -> et )

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

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 1006

This theorem is referenced by:  fvun1  5712  caseinl  7290  caseinr  7291  reapmul1  8775  recrecap  8889  rec11rap  8891  divdivdivap  8893  dmdcanap  8902  ddcanap  8906  rerecclap  8910  div2negap  8915  divap1d  8981  divmulapd  8992  apdivmuld  8993  divmulap2d  9004  divmulap3d  9005  divassapd  9006  div12apd  9007  div23apd  9008  divdirapd  9009  divsubdirapd  9010  div11apd  9011  ltmul12a  9040  ltdiv1  9048  ltrec  9063  lt2msq1  9065  lediv2  9071  lediv23  9073  recp1lt1  9079  qapne  9873  xadd4d  10120  xleaddadd  10122  modqge0  10595  modqlt  10596  modqid  10612  expgt1  10840  nnlesq  10906  expnbnd  10926  facubnd  11008  pfxsuffeqwrdeq  11283  resqrexlemover  11588  mulcn2  11890  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  eftlub  12269  eflegeo  12280  sin01bnd  12336  cos01bnd  12337  eirraplem  12356  bitsmod  12535  bezoutlemnewy  12585  bezoutlemstep  12586  mulgcd  12605  mulgcddvds  12684  prmind2  12710  oddpwdclemxy  12759  oddpwdclemodd  12762  qnumgt0  12788  pcpremul  12884  fldivp1  12939  pcfaclem  12940  qexpz  12943  prmpwdvds  12946  pockthg  12948  4sqlem10  12978  4sqlem12  12993  4sqlem16  12997  4sqlem17  12998  ablsub4  13918  znrrg  14693  txdis  15020  txdis1cn  15021  xblm  15160  reeff1oleme  15515  tangtx  15581  cosordlem  15592  logdivlti  15624  apcxp2  15682  mersenne  15740  lgsdilem  15775  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgsquadlem1  15825  lgsquadlem2  15826  2sqlem3  15865  2sqlem8  15871  0uhgrsubgr  16135  eupth2lem3lem3fi  16340  apdifflemr  16702