Theorem syl112anc 1253

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

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

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 982

This theorem is referenced by:  fvun1  5644  caseinl  7192  caseinr  7193  reapmul1  8667  recrecap  8781  rec11rap  8783  divdivdivap  8785  dmdcanap  8794  ddcanap  8798  rerecclap  8802  div2negap  8807  divap1d  8873  divmulapd  8884  apdivmuld  8885  divmulap2d  8896  divmulap3d  8897  divassapd  8898  div12apd  8899  div23apd  8900  divdirapd  8901  divsubdirapd  8902  div11apd  8903  ltmul12a  8932  ltdiv1  8940  ltrec  8955  lt2msq1  8957  lediv2  8963  lediv23  8965  recp1lt1  8971  qapne  9759  xadd4d  10006  xleaddadd  10008  modqge0  10475  modqlt  10476  modqid  10492  expgt1  10720  nnlesq  10786  expnbnd  10806  facubnd  10888  resqrexlemover  11292  mulcn2  11594  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  eftlub  11972  eflegeo  11983  sin01bnd  12039  cos01bnd  12040  eirraplem  12059  bitsmod  12238  bezoutlemnewy  12288  bezoutlemstep  12289  mulgcd  12308  mulgcddvds  12387  prmind2  12413  oddpwdclemxy  12462  oddpwdclemodd  12465  qnumgt0  12491  pcpremul  12587  fldivp1  12642  pcfaclem  12643  qexpz  12646  prmpwdvds  12649  pockthg  12651  4sqlem10  12681  4sqlem12  12696  4sqlem16  12700  4sqlem17  12701  ablsub4  13620  znrrg  14393  txdis  14720  txdis1cn  14721  xblm  14860  reeff1oleme  15215  tangtx  15281  cosordlem  15292  logdivlti  15324  apcxp2  15382  mersenne  15440  lgsdilem  15475  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgsquadlem1  15525  lgsquadlem2  15526  2sqlem3  15565  2sqlem8  15571  apdifflemr  15948