Theorem syl112anc 1254

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

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

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 983

This theorem is referenced by:  fvun1  5668  caseinl  7219  caseinr  7220  reapmul1  8703  recrecap  8817  rec11rap  8819  divdivdivap  8821  dmdcanap  8830  ddcanap  8834  rerecclap  8838  div2negap  8843  divap1d  8909  divmulapd  8920  apdivmuld  8921  divmulap2d  8932  divmulap3d  8933  divassapd  8934  div12apd  8935  div23apd  8936  divdirapd  8937  divsubdirapd  8938  div11apd  8939  ltmul12a  8968  ltdiv1  8976  ltrec  8991  lt2msq1  8993  lediv2  8999  lediv23  9001  recp1lt1  9007  qapne  9795  xadd4d  10042  xleaddadd  10044  modqge0  10514  modqlt  10515  modqid  10531  expgt1  10759  nnlesq  10825  expnbnd  10845  facubnd  10927  pfxsuffeqwrdeq  11189  resqrexlemover  11436  mulcn2  11738  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  eftlub  12116  eflegeo  12127  sin01bnd  12183  cos01bnd  12184  eirraplem  12203  bitsmod  12382  bezoutlemnewy  12432  bezoutlemstep  12433  mulgcd  12452  mulgcddvds  12531  prmind2  12557  oddpwdclemxy  12606  oddpwdclemodd  12609  qnumgt0  12635  pcpremul  12731  fldivp1  12786  pcfaclem  12787  qexpz  12790  prmpwdvds  12793  pockthg  12795  4sqlem10  12825  4sqlem12  12840  4sqlem16  12844  4sqlem17  12845  ablsub4  13764  znrrg  14537  txdis  14864  txdis1cn  14865  xblm  15004  reeff1oleme  15359  tangtx  15425  cosordlem  15436  logdivlti  15468  apcxp2  15526  mersenne  15584  lgsdilem  15619  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgsquadlem1  15669  lgsquadlem2  15670  2sqlem3  15709  2sqlem8  15715  apdifflemr  16188