Theorem syl112anc 1237

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 304	. 2 |- ( ph -> ( th /\ ta ) )
6		syl112anc.5	. 2 |- ( ( ps /\ ch /\ ( th /\ ta ) ) -> et )
7	1, 2, 5, 6	syl3anc 1233	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  fvun1  5562  caseinl  7068  caseinr  7069  reapmul1  8514  recrecap  8626  rec11rap  8628  divdivdivap  8630  dmdcanap  8639  ddcanap  8643  rerecclap  8647  div2negap  8652  divap1d  8718  divmulapd  8729  apdivmuld  8730  divmulap2d  8741  divmulap3d  8742  divassapd  8743  div12apd  8744  div23apd  8745  divdirapd  8746  divsubdirapd  8747  div11apd  8748  ltmul12a  8776  ltdiv1  8784  ltrec  8799  lt2msq1  8801  lediv2  8807  lediv23  8809  recp1lt1  8815  qapne  9598  xadd4d  9842  xleaddadd  9844  modqge0  10288  modqlt  10289  modqid  10305  expgt1  10514  nnlesq  10579  expnbnd  10599  facubnd  10679  resqrexlemover  10974  mulcn2  11275  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  eftlub  11653  eflegeo  11664  sin01bnd  11720  cos01bnd  11721  eirraplem  11739  bezoutlemnewy  11951  bezoutlemstep  11952  mulgcd  11971  mulgcddvds  12048  prmind2  12074  oddpwdclemxy  12123  oddpwdclemodd  12126  qnumgt0  12152  pcpremul  12247  fldivp1  12300  pcfaclem  12301  qexpz  12304  prmpwdvds  12307  pockthg  12309  4sqlem10  12339  txdis  13071  txdis1cn  13072  xblm  13211  reeff1oleme  13487  tangtx  13553  cosordlem  13564  logdivlti  13596  apcxp2  13652  lgsdilem  13722  2sqlem3  13747  2sqlem8  13753  apdifflemr  14079