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  5630  caseinl  7166  caseinr  7167  reapmul1  8639  recrecap  8753  rec11rap  8755  divdivdivap  8757  dmdcanap  8766  ddcanap  8770  rerecclap  8774  div2negap  8779  divap1d  8845  divmulapd  8856  apdivmuld  8857  divmulap2d  8868  divmulap3d  8869  divassapd  8870  div12apd  8871  div23apd  8872  divdirapd  8873  divsubdirapd  8874  div11apd  8875  ltmul12a  8904  ltdiv1  8912  ltrec  8927  lt2msq1  8929  lediv2  8935  lediv23  8937  recp1lt1  8943  qapne  9730  xadd4d  9977  xleaddadd  9979  modqge0  10441  modqlt  10442  modqid  10458  expgt1  10686  nnlesq  10752  expnbnd  10772  facubnd  10854  resqrexlemover  11192  mulcn2  11494  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  eftlub  11872  eflegeo  11883  sin01bnd  11939  cos01bnd  11940  eirraplem  11959  bitsmod  12138  bezoutlemnewy  12188  bezoutlemstep  12189  mulgcd  12208  mulgcddvds  12287  prmind2  12313  oddpwdclemxy  12362  oddpwdclemodd  12365  qnumgt0  12391  pcpremul  12487  fldivp1  12542  pcfaclem  12543  qexpz  12546  prmpwdvds  12549  pockthg  12551  4sqlem10  12581  4sqlem12  12596  4sqlem16  12600  4sqlem17  12601  ablsub4  13519  znrrg  14292  txdis  14597  txdis1cn  14598  xblm  14737  reeff1oleme  15092  tangtx  15158  cosordlem  15169  logdivlti  15201  apcxp2  15259  mersenne  15317  lgsdilem  15352  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgsquadlem1  15402  lgsquadlem2  15403  2sqlem3  15442  2sqlem8  15448  apdifflemr  15778