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  5772  caseinl  7437  caseinr  7438  reapmul1  8931  recrecap  9047  rec11rap  9049  divdivdivap  9051  dmdcanap  9060  ddcanap  9064  rerecclap  9068  div2negap  9073  divap1d  9139  divmulapd  9150  apdivmuld  9151  divmulap2d  9162  divmulap3d  9163  divassapd  9164  div12apd  9165  div23apd  9166  divdirapd  9167  divsubdirapd  9168  div11apd  9169  ltmul12a  9198  ltdiv1  9206  ltrec  9221  lt2msq1  9223  lediv2  9229  lediv23  9231  recp1lt1  9237  qapne  10054  xadd4d  10303  xleaddadd  10305  modqge0  10789  modqlt  10790  modqid  10806  expgt1  11034  nnlesq  11100  expnbnd  11121  facubnd  11204  pfxsuffeqwrdeq  11491  resqrexlemover  11797  mulcn2  12102  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  eftlub  12481  eflegeo  12492  sin01bnd  12548  cos01bnd  12549  eirraplem  12568  bitsmod  12747  bezoutlemnewy  12797  bezoutlemstep  12798  mulgcd  12817  mulgcddvds  12896  prmind2  12922  nnmaxpwlemxy  12972  nnmaxpwlemnfac  12975  qnumgt0  13002  pcpremul  13100  fldivp1  13155  pcfaclem  13156  qexpz  13159  prmpwdvds  13162  pockthg  13164  4sqlem10  13194  4sqlem12  13209  4sqlem16  13213  4sqlem17  13214  ablsub4  14206  znrrg  15103  txdis  15520  txdis1cn  15521  xblm  15660  reeff1oleme  16015  tangtx  16082  cosordlem  16094  logdivlti  16128  apcxp2  16191  zprmlogbaplem3  16234  log2tlbndlog2  16237  birthdaylem3  16244  pellexlem2  16247  ppiqub  16310  mersenne  16314  bposlem1  16328  bposlem2  16329  bposlem4  16331  lgsdilem  16368  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgsquadlem1  16418  lgsquadlem2  16419  2sqlem3  16458  2sqlem8  16464  0uhgrsubgr  16728  eupth2lem3lem3fi  16933  apdifflemr  17320