Theorem syl112anc 1242

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 1238	1 |- ( ph -> et )

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

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 980

This theorem is referenced by:  fvun1  5583  caseinl  7090  caseinr  7091  reapmul1  8552  recrecap  8666  rec11rap  8668  divdivdivap  8670  dmdcanap  8679  ddcanap  8683  rerecclap  8687  div2negap  8692  divap1d  8758  divmulapd  8769  apdivmuld  8770  divmulap2d  8781  divmulap3d  8782  divassapd  8783  div12apd  8784  div23apd  8785  divdirapd  8786  divsubdirapd  8787  div11apd  8788  ltmul12a  8817  ltdiv1  8825  ltrec  8840  lt2msq1  8842  lediv2  8848  lediv23  8850  recp1lt1  8856  qapne  9639  xadd4d  9885  xleaddadd  9887  modqge0  10332  modqlt  10333  modqid  10349  expgt1  10558  nnlesq  10624  expnbnd  10644  facubnd  10725  resqrexlemover  11019  mulcn2  11320  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  eftlub  11698  eflegeo  11709  sin01bnd  11765  cos01bnd  11766  eirraplem  11784  bezoutlemnewy  11997  bezoutlemstep  11998  mulgcd  12017  mulgcddvds  12094  prmind2  12120  oddpwdclemxy  12169  oddpwdclemodd  12172  qnumgt0  12198  pcpremul  12293  fldivp1  12346  pcfaclem  12347  qexpz  12350  prmpwdvds  12353  pockthg  12355  4sqlem10  12385  ablsub4  13116  txdis  13780  txdis1cn  13781  xblm  13920  reeff1oleme  14196  tangtx  14262  cosordlem  14273  logdivlti  14305  apcxp2  14361  lgsdilem  14431  lgseisenlem1  14453  lgseisenlem2  14454  2sqlem3  14467  2sqlem8  14473  apdifflemr  14798