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  5627  caseinl  7157  caseinr  7158  reapmul1  8622  recrecap  8736  rec11rap  8738  divdivdivap  8740  dmdcanap  8749  ddcanap  8753  rerecclap  8757  div2negap  8762  divap1d  8828  divmulapd  8839  apdivmuld  8840  divmulap2d  8851  divmulap3d  8852  divassapd  8853  div12apd  8854  div23apd  8855  divdirapd  8856  divsubdirapd  8857  div11apd  8858  ltmul12a  8887  ltdiv1  8895  ltrec  8910  lt2msq1  8912  lediv2  8918  lediv23  8920  recp1lt1  8926  qapne  9713  xadd4d  9960  xleaddadd  9962  modqge0  10424  modqlt  10425  modqid  10441  expgt1  10669  nnlesq  10735  expnbnd  10755  facubnd  10837  resqrexlemover  11175  mulcn2  11477  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  eftlub  11855  eflegeo  11866  sin01bnd  11922  cos01bnd  11923  eirraplem  11942  bezoutlemnewy  12163  bezoutlemstep  12164  mulgcd  12183  mulgcddvds  12262  prmind2  12288  oddpwdclemxy  12337  oddpwdclemodd  12340  qnumgt0  12366  pcpremul  12462  fldivp1  12517  pcfaclem  12518  qexpz  12521  prmpwdvds  12524  pockthg  12526  4sqlem10  12556  4sqlem12  12571  4sqlem16  12575  4sqlem17  12576  ablsub4  13443  znrrg  14216  txdis  14513  txdis1cn  14514  xblm  14653  reeff1oleme  15008  tangtx  15074  cosordlem  15085  logdivlti  15117  apcxp2  15175  mersenne  15233  lgsdilem  15268  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgsquadlem1  15318  lgsquadlem2  15319  2sqlem3  15358  2sqlem8  15364  apdifflemr  15691