Theorem syl112anc 1232

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 304	. 2 |- ( ph -> ( th /\ ta ) )
6		syl112anc.5	. 2 |- ( ( ps /\ ch /\ ( th /\ ta ) ) -> et )
7	1, 2, 5, 6	syl3anc 1228	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  fvun1  5551  caseinl  7052  caseinr  7053  reapmul1  8489  recrecap  8601  rec11rap  8603  divdivdivap  8605  dmdcanap  8614  ddcanap  8618  rerecclap  8622  div2negap  8627  divap1d  8693  divmulapd  8704  apdivmuld  8705  divmulap2d  8716  divmulap3d  8717  divassapd  8718  div12apd  8719  div23apd  8720  divdirapd  8721  divsubdirapd  8722  div11apd  8723  ltmul12a  8751  ltdiv1  8759  ltrec  8774  lt2msq1  8776  lediv2  8782  lediv23  8784  recp1lt1  8790  qapne  9573  xadd4d  9817  xleaddadd  9819  modqge0  10263  modqlt  10264  modqid  10280  expgt1  10489  nnlesq  10554  expnbnd  10574  facubnd  10654  resqrexlemover  10948  mulcn2  11249  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  eftlub  11627  eflegeo  11638  sin01bnd  11694  cos01bnd  11695  eirraplem  11713  bezoutlemnewy  11925  bezoutlemstep  11926  mulgcd  11945  mulgcddvds  12022  prmind2  12048  oddpwdclemxy  12097  oddpwdclemodd  12100  qnumgt0  12126  pcpremul  12221  fldivp1  12274  pcfaclem  12275  qexpz  12278  prmpwdvds  12281  pockthg  12283  4sqlem10  12313  txdis  12877  txdis1cn  12878  xblm  13017  reeff1oleme  13293  tangtx  13359  cosordlem  13370  logdivlti  13402  apcxp2  13458  lgsdilem  13528  2sqlem3  13553  2sqlem8  13559  apdifflemr  13886