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  7431  caseinr  7432  reapmul1  8923  recrecap  9039  rec11rap  9041  divdivdivap  9043  dmdcanap  9052  ddcanap  9056  rerecclap  9060  div2negap  9065  divap1d  9131  divmulapd  9142  apdivmuld  9143  divmulap2d  9154  divmulap3d  9155  divassapd  9156  div12apd  9157  div23apd  9158  divdirapd  9159  divsubdirapd  9160  div11apd  9161  ltmul12a  9190  ltdiv1  9198  ltrec  9213  lt2msq1  9215  lediv2  9221  lediv23  9223  recp1lt1  9229  qapne  10039  xadd4d  10287  xleaddadd  10289  modqge0  10769  modqlt  10770  modqid  10786  expgt1  11014  nnlesq  11080  expnbnd  11101  facubnd  11183  pfxsuffeqwrdeq  11470  resqrexlemover  11776  mulcn2  12078  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  eftlub  12457  eflegeo  12468  sin01bnd  12524  cos01bnd  12525  eirraplem  12544  bitsmod  12723  bezoutlemnewy  12773  bezoutlemstep  12774  mulgcd  12793  mulgcddvds  12872  prmind2  12898  oddpwdclemxy  12947  oddpwdclemodd  12950  qnumgt0  12976  pcpremul  13072  fldivp1  13127  pcfaclem  13128  qexpz  13131  prmpwdvds  13134  pockthg  13136  4sqlem10  13166  4sqlem12  13181  4sqlem16  13185  4sqlem17  13186  ablsub4  14117  znrrg  14995  txdis  15378  txdis1cn  15379  xblm  15518  reeff1oleme  15873  tangtx  15939  cosordlem  15950  logdivlti  15982  apcxp2  16041  log2tlbndlog2  16082  birthdaylem3  16089  pellexlem2  16092  mersenne  16111  lgsdilem  16146  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgsquadlem1  16196  lgsquadlem2  16197  2sqlem3  16236  2sqlem8  16242  0uhgrsubgr  16506  eupth2lem3lem3fi  16711  apdifflemr  17096