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  5599  caseinl  7115  caseinr  7116  reapmul1  8577  recrecap  8691  rec11rap  8693  divdivdivap  8695  dmdcanap  8704  ddcanap  8708  rerecclap  8712  div2negap  8717  divap1d  8783  divmulapd  8794  apdivmuld  8795  divmulap2d  8806  divmulap3d  8807  divassapd  8808  div12apd  8809  div23apd  8810  divdirapd  8811  divsubdirapd  8812  div11apd  8813  ltmul12a  8842  ltdiv1  8850  ltrec  8865  lt2msq1  8867  lediv2  8873  lediv23  8875  recp1lt1  8881  qapne  9664  xadd4d  9910  xleaddadd  9912  modqge0  10358  modqlt  10359  modqid  10375  expgt1  10584  nnlesq  10650  expnbnd  10670  facubnd  10752  resqrexlemover  11046  mulcn2  11347  cvgratnnlemnexp  11559  cvgratnnlemmn  11560  eftlub  11725  eflegeo  11736  sin01bnd  11792  cos01bnd  11793  eirraplem  11811  bezoutlemnewy  12024  bezoutlemstep  12025  mulgcd  12044  mulgcddvds  12121  prmind2  12147  oddpwdclemxy  12196  oddpwdclemodd  12199  qnumgt0  12225  pcpremul  12320  fldivp1  12375  pcfaclem  12376  qexpz  12379  prmpwdvds  12382  pockthg  12384  4sqlem10  12414  4sqlem12  12429  4sqlem16  12433  4sqlem17  12434  ablsub4  13245  txdis  14214  txdis1cn  14215  xblm  14354  reeff1oleme  14630  tangtx  14696  cosordlem  14707  logdivlti  14739  apcxp2  14795  lgsdilem  14865  lgseisenlem1  14887  lgseisenlem2  14888  2sqlem3  14901  2sqlem8  14907  apdifflemr  15233