Theorem syl112anc 1277

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

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

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 1006

This theorem is referenced by:  fvun1  5712  caseinl  7289  caseinr  7290  reapmul1  8774  recrecap  8888  rec11rap  8890  divdivdivap  8892  dmdcanap  8901  ddcanap  8905  rerecclap  8909  div2negap  8914  divap1d  8980  divmulapd  8991  apdivmuld  8992  divmulap2d  9003  divmulap3d  9004  divassapd  9005  div12apd  9006  div23apd  9007  divdirapd  9008  divsubdirapd  9009  div11apd  9010  ltmul12a  9039  ltdiv1  9047  ltrec  9062  lt2msq1  9064  lediv2  9070  lediv23  9072  recp1lt1  9078  qapne  9872  xadd4d  10119  xleaddadd  10121  modqge0  10593  modqlt  10594  modqid  10610  expgt1  10838  nnlesq  10904  expnbnd  10924  facubnd  11006  pfxsuffeqwrdeq  11278  resqrexlemover  11570  mulcn2  11872  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  eftlub  12250  eflegeo  12261  sin01bnd  12317  cos01bnd  12318  eirraplem  12337  bitsmod  12516  bezoutlemnewy  12566  bezoutlemstep  12567  mulgcd  12586  mulgcddvds  12665  prmind2  12691  oddpwdclemxy  12740  oddpwdclemodd  12743  qnumgt0  12769  pcpremul  12865  fldivp1  12920  pcfaclem  12921  qexpz  12924  prmpwdvds  12927  pockthg  12929  4sqlem10  12959  4sqlem12  12974  4sqlem16  12978  4sqlem17  12979  ablsub4  13899  znrrg  14673  txdis  15000  txdis1cn  15001  xblm  15140  reeff1oleme  15495  tangtx  15561  cosordlem  15572  logdivlti  15604  apcxp2  15662  mersenne  15720  lgsdilem  15755  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgsquadlem1  15805  lgsquadlem2  15806  2sqlem3  15845  2sqlem8  15851  0uhgrsubgr  16115  apdifflemr  16651