Theorem syl112anc 1188

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

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

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

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

This theorem is referenced by:  fvun1  5419  caseinl  6891  caseinr  6892  reapmul1  8223  recrecap  8330  rec11rap  8332  divdivdivap  8334  dmdcanap  8343  ddcanap  8347  rerecclap  8351  div2negap  8356  divap1d  8422  divmulapd  8433  apdivmuld  8434  divmulap2d  8445  divmulap3d  8446  divassapd  8447  div12apd  8448  div23apd  8449  divdirapd  8450  divsubdirapd  8451  div11apd  8452  ltmul12a  8476  ltdiv1  8484  ltrec  8499  lt2msq1  8501  lediv2  8507  lediv23  8509  recp1lt1  8515  qapne  9281  xadd4d  9509  xleaddadd  9511  modqge0  9946  modqlt  9947  modqid  9963  expgt1  10172  nnlesq  10237  expnbnd  10256  facubnd  10332  resqrexlemover  10622  mulcn2  10920  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  eftlub  11194  eflegeo  11206  sin01bnd  11262  cos01bnd  11263  eirraplem  11278  bezoutlemnewy  11477  bezoutlemstep  11478  mulgcd  11497  mulgcddvds  11568  prmind2  11594  oddpwdclemxy  11639  oddpwdclemodd  11642  qnumgt0  11668  txdis  12227  txdis1cn  12228  xblm  12345