Theorem syl112anc 1282

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fvun1  5769  caseinl  7432  caseinr  7433  reapmul1  8926  recrecap  9042  rec11rap  9044  divdivdivap  9046  dmdcanap  9055  ddcanap  9059  rerecclap  9063  div2negap  9068  divap1d  9134  divmulapd  9145  apdivmuld  9146  divmulap2d  9157  divmulap3d  9158  divassapd  9159  div12apd  9160  div23apd  9161  divdirapd  9162  divsubdirapd  9163  div11apd  9164  ltmul12a  9193  ltdiv1  9201  ltrec  9216  lt2msq1  9218  lediv2  9224  lediv23  9226  recp1lt1  9232  qapne  10049  xadd4d  10298  xleaddadd  10300  modqge0  10784  modqlt  10785  modqid  10801  expgt1  11029  nnlesq  11095  expnbnd  11116  facubnd  11199  pfxsuffeqwrdeq  11486  resqrexlemover  11792  mulcn2  12097  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  eftlub  12476  eflegeo  12487  sin01bnd  12543  cos01bnd  12544  eirraplem  12563  bitsmod  12742  bezoutlemnewy  12792  bezoutlemstep  12793  mulgcd  12812  mulgcddvds  12891  prmind2  12917  nnmaxpwlemxy  12967  nnmaxpwlemnfac  12970  qnumgt0  12997  pcpremul  13095  fldivp1  13150  pcfaclem  13151  qexpz  13154  prmpwdvds  13157  pockthg  13159  4sqlem10  13189  4sqlem12  13204  4sqlem16  13208  4sqlem17  13209  ablsub4  14201  znrrg  15079  txdis  15469  txdis1cn  15470  xblm  15609  reeff1oleme  15964  tangtx  16031  cosordlem  16042  logdivlti  16075  apcxp2  16136  zprmlogbaplem3  16178  log2tlbndlog2  16181  birthdaylem3  16188  pellexlem2  16191  ppiqub  16254  mersenne  16258  bposlem1  16272  bposlem2  16273  bposlem4  16275  lgsdilem  16312  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgsquadlem1  16362  lgsquadlem2  16363  2sqlem3  16402  2sqlem8  16408  0uhgrsubgr  16672  eupth2lem3lem3fi  16877  apdifflemr  17263