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  5748  caseinl  7395  caseinr  7396  reapmul1  8886  recrecap  9000  rec11rap  9002  divdivdivap  9004  dmdcanap  9013  ddcanap  9017  rerecclap  9021  div2negap  9026  divap1d  9092  divmulapd  9103  apdivmuld  9104  divmulap2d  9115  divmulap3d  9116  divassapd  9117  div12apd  9118  div23apd  9119  divdirapd  9120  divsubdirapd  9121  div11apd  9122  ltmul12a  9151  ltdiv1  9159  ltrec  9174  lt2msq1  9176  lediv2  9182  lediv23  9184  recp1lt1  9190  qapne  9989  xadd4d  10237  xleaddadd  10239  modqge0  10718  modqlt  10719  modqid  10735  expgt1  10963  nnlesq  11029  expnbnd  11050  facubnd  11132  pfxsuffeqwrdeq  11415  resqrexlemover  11720  mulcn2  12022  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  eftlub  12401  eflegeo  12412  sin01bnd  12468  cos01bnd  12469  eirraplem  12488  bitsmod  12667  bezoutlemnewy  12717  bezoutlemstep  12718  mulgcd  12737  mulgcddvds  12816  prmind2  12842  oddpwdclemxy  12891  oddpwdclemodd  12894  qnumgt0  12920  pcpremul  13016  fldivp1  13071  pcfaclem  13072  qexpz  13075  prmpwdvds  13078  pockthg  13080  4sqlem10  13110  4sqlem12  13125  4sqlem16  13129  4sqlem17  13130  ablsub4  14066  znrrg  14934  txdis  15268  txdis1cn  15269  xblm  15408  reeff1oleme  15763  tangtx  15829  cosordlem  15840  logdivlti  15872  apcxp2  15930  pellexlem2  15972  mersenne  15991  lgsdilem  16026  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgsquadlem1  16076  lgsquadlem2  16077  2sqlem3  16116  2sqlem8  16122  0uhgrsubgr  16386  eupth2lem3lem3fi  16591  apdifflemr  16957