Theorem syl112anc 1253

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

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

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 982

This theorem is referenced by:  fvun1  5623  caseinl  7150  caseinr  7151  reapmul1  8614  recrecap  8728  rec11rap  8730  divdivdivap  8732  dmdcanap  8741  ddcanap  8745  rerecclap  8749  div2negap  8754  divap1d  8820  divmulapd  8831  apdivmuld  8832  divmulap2d  8843  divmulap3d  8844  divassapd  8845  div12apd  8846  div23apd  8847  divdirapd  8848  divsubdirapd  8849  div11apd  8850  ltmul12a  8879  ltdiv1  8887  ltrec  8902  lt2msq1  8904  lediv2  8910  lediv23  8912  recp1lt1  8918  qapne  9704  xadd4d  9951  xleaddadd  9953  modqge0  10403  modqlt  10404  modqid  10420  expgt1  10648  nnlesq  10714  expnbnd  10734  facubnd  10816  resqrexlemover  11154  mulcn2  11455  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  eftlub  11833  eflegeo  11844  sin01bnd  11900  cos01bnd  11901  eirraplem  11920  bezoutlemnewy  12133  bezoutlemstep  12134  mulgcd  12153  mulgcddvds  12232  prmind2  12258  oddpwdclemxy  12307  oddpwdclemodd  12310  qnumgt0  12336  pcpremul  12431  fldivp1  12486  pcfaclem  12487  qexpz  12490  prmpwdvds  12493  pockthg  12495  4sqlem10  12525  4sqlem12  12540  4sqlem16  12544  4sqlem17  12545  ablsub4  13383  znrrg  14148  txdis  14445  txdis1cn  14446  xblm  14585  reeff1oleme  14907  tangtx  14973  cosordlem  14984  logdivlti  15016  apcxp2  15072  lgsdilem  15143  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgsquadlem1  15191  2sqlem3  15204  2sqlem8  15210  apdifflemr  15537