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  10055  xadd4d  10304  xleaddadd  10306  modqge0  10790  modqlt  10791  modqid  10807  expgt1  11035  nnlesq  11101  expnbnd  11122  facubnd  11205  pfxsuffeqwrdeq  11492  resqrexlemover  11798  mulcn2  12103  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  eftlub  12482  eflegeo  12493  sin01bnd  12549  cos01bnd  12550  eirraplem  12569  bitsmod  12748  bezoutlemnewy  12798  bezoutlemstep  12799  mulgcd  12818  mulgcddvds  12897  prmind2  12923  nnmaxpwlemxy  12973  nnmaxpwlemnfac  12976  qnumgt0  13003  pcpremul  13101  fldivp1  13156  pcfaclem  13157  qexpz  13160  prmpwdvds  13163  pockthg  13165  4sqlem10  13195  4sqlem12  13210  4sqlem16  13214  4sqlem17  13215  ablsub4  14207  znrrg  15104  txdis  15503  txdis1cn  15504  xblm  15643  reeff1oleme  15998  tangtx  16065  cosordlem  16077  logdivlti  16111  apcxp2  16174  zprmlogbaplem3  16217  log2tlbndlog2  16220  birthdaylem3  16227  pellexlem2  16230  ppiqub  16293  mersenne  16297  bposlem1  16311  bposlem2  16312  bposlem4  16314  lgsdilem  16351  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgsquadlem1  16401  lgsquadlem2  16402  2sqlem3  16441  2sqlem8  16447  0uhgrsubgr  16711  eupth2lem3lem3fi  16916  apdifflemr  17303