Theorem syl112anc 1282

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fvun1  5769  caseinl  7431  caseinr  7432  reapmul1  8925  recrecap  9041  rec11rap  9043  divdivdivap  9045  dmdcanap  9054  ddcanap  9058  rerecclap  9062  div2negap  9067  divap1d  9133  divmulapd  9144  apdivmuld  9145  divmulap2d  9156  divmulap3d  9157  divassapd  9158  div12apd  9159  div23apd  9160  divdirapd  9161  divsubdirapd  9162  div11apd  9163  ltmul12a  9192  ltdiv1  9200  ltrec  9215  lt2msq1  9217  lediv2  9223  lediv23  9225  recp1lt1  9231  qapne  10048  xadd4d  10297  xleaddadd  10299  modqge0  10782  modqlt  10783  modqid  10799  expgt1  11027  nnlesq  11093  expnbnd  11114  facubnd  11197  pfxsuffeqwrdeq  11484  resqrexlemover  11790  mulcn2  12094  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  eftlub  12473  eflegeo  12484  sin01bnd  12540  cos01bnd  12541  eirraplem  12560  bitsmod  12739  bezoutlemnewy  12789  bezoutlemstep  12790  mulgcd  12809  mulgcddvds  12888  prmind2  12914  nnmaxpwlemxy  12964  nnmaxpwlemnfac  12967  qnumgt0  12994  pcpremul  13092  fldivp1  13147  pcfaclem  13148  qexpz  13151  prmpwdvds  13154  pockthg  13156  4sqlem10  13186  4sqlem12  13201  4sqlem16  13205  4sqlem17  13206  ablsub4  14166  znrrg  15044  txdis  15427  txdis1cn  15428  xblm  15567  reeff1oleme  15922  tangtx  15989  cosordlem  16000  logdivlti  16033  apcxp2  16094  zprmlogbaplem3  16136  log2tlbndlog2  16139  birthdaylem3  16146  pellexlem2  16149  ppiqub  16194  mersenne  16195  bposlem1  16209  bposlem2  16210  bposlem4  16212  lgsdilem  16244  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgsquadlem1  16294  lgsquadlem2  16295  2sqlem3  16334  2sqlem8  16340  0uhgrsubgr  16604  eupth2lem3lem3fi  16809  apdifflemr  17194