Theorem syl112anc 1278

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

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

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 1007

This theorem is referenced by:  fvun1  5721  caseinl  7333  caseinr  7334  reapmul1  8817  recrecap  8931  rec11rap  8933  divdivdivap  8935  dmdcanap  8944  ddcanap  8948  rerecclap  8952  div2negap  8957  divap1d  9023  divmulapd  9034  apdivmuld  9035  divmulap2d  9046  divmulap3d  9047  divassapd  9048  div12apd  9049  div23apd  9050  divdirapd  9051  divsubdirapd  9052  div11apd  9053  ltmul12a  9082  ltdiv1  9090  ltrec  9105  lt2msq1  9107  lediv2  9113  lediv23  9115  recp1lt1  9121  qapne  9917  xadd4d  10164  xleaddadd  10166  modqge0  10640  modqlt  10641  modqid  10657  expgt1  10885  nnlesq  10951  expnbnd  10971  facubnd  11053  pfxsuffeqwrdeq  11328  resqrexlemover  11633  mulcn2  11935  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  eftlub  12314  eflegeo  12325  sin01bnd  12381  cos01bnd  12382  eirraplem  12401  bitsmod  12580  bezoutlemnewy  12630  bezoutlemstep  12631  mulgcd  12650  mulgcddvds  12729  prmind2  12755  oddpwdclemxy  12804  oddpwdclemodd  12807  qnumgt0  12833  pcpremul  12929  fldivp1  12984  pcfaclem  12985  qexpz  12988  prmpwdvds  12991  pockthg  12993  4sqlem10  13023  4sqlem12  13038  4sqlem16  13042  4sqlem17  13043  ablsub4  13963  znrrg  14739  txdis  15071  txdis1cn  15072  xblm  15211  reeff1oleme  15566  tangtx  15632  cosordlem  15643  logdivlti  15675  apcxp2  15733  pellexlem2  15775  mersenne  15794  lgsdilem  15829  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgsquadlem1  15879  lgsquadlem2  15880  2sqlem3  15919  2sqlem8  15925  0uhgrsubgr  16189  eupth2lem3lem3fi  16394  apdifflemr  16762