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  5663  caseinl  7214  caseinr  7215  reapmul1  8698  recrecap  8812  rec11rap  8814  divdivdivap  8816  dmdcanap  8825  ddcanap  8829  rerecclap  8833  div2negap  8838  divap1d  8904  divmulapd  8915  apdivmuld  8916  divmulap2d  8927  divmulap3d  8928  divassapd  8929  div12apd  8930  div23apd  8931  divdirapd  8932  divsubdirapd  8933  div11apd  8934  ltmul12a  8963  ltdiv1  8971  ltrec  8986  lt2msq1  8988  lediv2  8994  lediv23  8996  recp1lt1  9002  qapne  9790  xadd4d  10037  xleaddadd  10039  modqge0  10509  modqlt  10510  modqid  10526  expgt1  10754  nnlesq  10820  expnbnd  10840  facubnd  10922  pfxsuffeqwrdeq  11184  resqrexlemover  11406  mulcn2  11708  cvgratnnlemnexp  11920  cvgratnnlemmn  11921  eftlub  12086  eflegeo  12097  sin01bnd  12153  cos01bnd  12154  eirraplem  12173  bitsmod  12352  bezoutlemnewy  12402  bezoutlemstep  12403  mulgcd  12422  mulgcddvds  12501  prmind2  12527  oddpwdclemxy  12576  oddpwdclemodd  12579  qnumgt0  12605  pcpremul  12701  fldivp1  12756  pcfaclem  12757  qexpz  12760  prmpwdvds  12763  pockthg  12765  4sqlem10  12795  4sqlem12  12810  4sqlem16  12814  4sqlem17  12815  ablsub4  13734  znrrg  14507  txdis  14834  txdis1cn  14835  xblm  14974  reeff1oleme  15329  tangtx  15395  cosordlem  15406  logdivlti  15438  apcxp2  15496  mersenne  15554  lgsdilem  15589  lgseisenlem1  15632  lgseisenlem2  15633  lgseisenlem3  15634  lgsquadlem1  15639  lgsquadlem2  15640  2sqlem3  15679  2sqlem8  15685  apdifflemr  16158