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  5702  caseinl  7269  caseinr  7270  reapmul1  8753  recrecap  8867  rec11rap  8869  divdivdivap  8871  dmdcanap  8880  ddcanap  8884  rerecclap  8888  div2negap  8893  divap1d  8959  divmulapd  8970  apdivmuld  8971  divmulap2d  8982  divmulap3d  8983  divassapd  8984  div12apd  8985  div23apd  8986  divdirapd  8987  divsubdirapd  8988  div11apd  8989  ltmul12a  9018  ltdiv1  9026  ltrec  9041  lt2msq1  9043  lediv2  9049  lediv23  9051  recp1lt1  9057  qapne  9846  xadd4d  10093  xleaddadd  10095  modqge0  10566  modqlt  10567  modqid  10583  expgt1  10811  nnlesq  10877  expnbnd  10897  facubnd  10979  pfxsuffeqwrdeq  11245  resqrexlemover  11536  mulcn2  11838  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  eftlub  12216  eflegeo  12227  sin01bnd  12283  cos01bnd  12284  eirraplem  12303  bitsmod  12482  bezoutlemnewy  12532  bezoutlemstep  12533  mulgcd  12552  mulgcddvds  12631  prmind2  12657  oddpwdclemxy  12706  oddpwdclemodd  12709  qnumgt0  12735  pcpremul  12831  fldivp1  12886  pcfaclem  12887  qexpz  12890  prmpwdvds  12893  pockthg  12895  4sqlem10  12925  4sqlem12  12940  4sqlem16  12944  4sqlem17  12945  ablsub4  13865  znrrg  14639  txdis  14966  txdis1cn  14967  xblm  15106  reeff1oleme  15461  tangtx  15527  cosordlem  15538  logdivlti  15570  apcxp2  15628  mersenne  15686  lgsdilem  15721  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgsquadlem1  15771  lgsquadlem2  15772  2sqlem3  15811  2sqlem8  15817  apdifflemr  16475