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  5743  caseinl  7382  caseinr  7383  reapmul1  8869  recrecap  8983  rec11rap  8985  divdivdivap  8987  dmdcanap  8996  ddcanap  9000  rerecclap  9004  div2negap  9009  divap1d  9075  divmulapd  9086  apdivmuld  9087  divmulap2d  9098  divmulap3d  9099  divassapd  9100  div12apd  9101  div23apd  9102  divdirapd  9103  divsubdirapd  9104  div11apd  9105  ltmul12a  9134  ltdiv1  9142  ltrec  9157  lt2msq1  9159  lediv2  9165  lediv23  9167  recp1lt1  9173  qapne  9971  xadd4d  10218  xleaddadd  10220  modqge0  10694  modqlt  10695  modqid  10711  expgt1  10939  nnlesq  11005  expnbnd  11025  facubnd  11107  pfxsuffeqwrdeq  11390  resqrexlemover  11695  mulcn2  11997  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  eftlub  12376  eflegeo  12387  sin01bnd  12443  cos01bnd  12444  eirraplem  12463  bitsmod  12642  bezoutlemnewy  12692  bezoutlemstep  12693  mulgcd  12712  mulgcddvds  12791  prmind2  12817  oddpwdclemxy  12866  oddpwdclemodd  12869  qnumgt0  12895  pcpremul  12991  fldivp1  13046  pcfaclem  13047  qexpz  13050  prmpwdvds  13053  pockthg  13055  4sqlem10  13085  4sqlem12  13100  4sqlem16  13104  4sqlem17  13105  ablsub4  14030  znrrg  14808  txdis  15142  txdis1cn  15143  xblm  15282  reeff1oleme  15637  tangtx  15703  cosordlem  15714  logdivlti  15746  apcxp2  15804  pellexlem2  15846  mersenne  15865  lgsdilem  15900  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgsquadlem1  15950  lgsquadlem2  15951  2sqlem3  15990  2sqlem8  15996  0uhgrsubgr  16260  eupth2lem3lem3fi  16465  apdifflemr  16831