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 )

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

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 1011

This theorem is referenced by:  fvun1  5763  caseinl  7421  caseinr  7422  reapmul1  8913  recrecap  9029  rec11rap  9031  divdivdivap  9033  dmdcanap  9042  ddcanap  9046  rerecclap  9050  div2negap  9055  divap1d  9121  divmulapd  9132  apdivmuld  9133  divmulap2d  9144  divmulap3d  9145  divassapd  9146  div12apd  9147  div23apd  9148  divdirapd  9149  divsubdirapd  9150  div11apd  9151  ltmul12a  9180  ltdiv1  9188  ltrec  9203  lt2msq1  9205  lediv2  9211  lediv23  9213  recp1lt1  9219  qapne  10018  xadd4d  10266  xleaddadd  10268  modqge0  10747  modqlt  10748  modqid  10764  expgt1  10992  nnlesq  11058  expnbnd  11079  facubnd  11161  pfxsuffeqwrdeq  11448  resqrexlemover  11754  mulcn2  12056  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  eftlub  12435  eflegeo  12446  sin01bnd  12502  cos01bnd  12503  eirraplem  12522  bitsmod  12701  bezoutlemnewy  12751  bezoutlemstep  12752  mulgcd  12771  mulgcddvds  12850  prmind2  12876  oddpwdclemxy  12925  oddpwdclemodd  12928  qnumgt0  12954  pcpremul  13050  fldivp1  13105  pcfaclem  13106  qexpz  13109  prmpwdvds  13112  pockthg  13114  4sqlem10  13144  4sqlem12  13159  4sqlem16  13163  4sqlem17  13164  ablsub4  14094  znrrg  14967  txdis  15301  txdis1cn  15302  xblm  15441  reeff1oleme  15796  tangtx  15862  cosordlem  15873  logdivlti  15905  apcxp2  15964  pellexlem2  16006  mersenne  16025  lgsdilem  16060  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgsquadlem1  16110  lgsquadlem2  16111  2sqlem3  16150  2sqlem8  16156  0uhgrsubgr  16420  eupth2lem3lem3fi  16625  apdifflemr  17001