Theorem syl112anc 1275

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

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

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 1004

This theorem is referenced by:  fvun1  5699  caseinl  7254  caseinr  7255  reapmul1  8738  recrecap  8852  rec11rap  8854  divdivdivap  8856  dmdcanap  8865  ddcanap  8869  rerecclap  8873  div2negap  8878  divap1d  8944  divmulapd  8955  apdivmuld  8956  divmulap2d  8967  divmulap3d  8968  divassapd  8969  div12apd  8970  div23apd  8971  divdirapd  8972  divsubdirapd  8973  div11apd  8974  ltmul12a  9003  ltdiv1  9011  ltrec  9026  lt2msq1  9028  lediv2  9034  lediv23  9036  recp1lt1  9042  qapne  9830  xadd4d  10077  xleaddadd  10079  modqge0  10549  modqlt  10550  modqid  10566  expgt1  10794  nnlesq  10860  expnbnd  10880  facubnd  10962  pfxsuffeqwrdeq  11225  resqrexlemover  11516  mulcn2  11818  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  eftlub  12196  eflegeo  12207  sin01bnd  12263  cos01bnd  12264  eirraplem  12283  bitsmod  12462  bezoutlemnewy  12512  bezoutlemstep  12513  mulgcd  12532  mulgcddvds  12611  prmind2  12637  oddpwdclemxy  12686  oddpwdclemodd  12689  qnumgt0  12715  pcpremul  12811  fldivp1  12866  pcfaclem  12867  qexpz  12870  prmpwdvds  12873  pockthg  12875  4sqlem10  12905  4sqlem12  12920  4sqlem16  12924  4sqlem17  12925  ablsub4  13845  znrrg  14618  txdis  14945  txdis1cn  14946  xblm  15085  reeff1oleme  15440  tangtx  15506  cosordlem  15517  logdivlti  15549  apcxp2  15607  mersenne  15665  lgsdilem  15700  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgsquadlem1  15750  lgsquadlem2  15751  2sqlem3  15790  2sqlem8  15796  apdifflemr  16374