Theorem syl112anc 1237

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

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

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 975

This theorem is referenced by:  fvun1  5560  caseinl  7064  caseinr  7065  reapmul1  8501  recrecap  8613  rec11rap  8615  divdivdivap  8617  dmdcanap  8626  ddcanap  8630  rerecclap  8634  div2negap  8639  divap1d  8705  divmulapd  8716  apdivmuld  8717  divmulap2d  8728  divmulap3d  8729  divassapd  8730  div12apd  8731  div23apd  8732  divdirapd  8733  divsubdirapd  8734  div11apd  8735  ltmul12a  8763  ltdiv1  8771  ltrec  8786  lt2msq1  8788  lediv2  8794  lediv23  8796  recp1lt1  8802  qapne  9585  xadd4d  9829  xleaddadd  9831  modqge0  10275  modqlt  10276  modqid  10292  expgt1  10501  nnlesq  10566  expnbnd  10586  facubnd  10666  resqrexlemover  10961  mulcn2  11262  cvgratnnlemnexp  11474  cvgratnnlemmn  11475  eftlub  11640  eflegeo  11651  sin01bnd  11707  cos01bnd  11708  eirraplem  11726  bezoutlemnewy  11938  bezoutlemstep  11939  mulgcd  11958  mulgcddvds  12035  prmind2  12061  oddpwdclemxy  12110  oddpwdclemodd  12113  qnumgt0  12139  pcpremul  12234  fldivp1  12287  pcfaclem  12288  qexpz  12291  prmpwdvds  12294  pockthg  12296  4sqlem10  12326  txdis  13030  txdis1cn  13031  xblm  13170  reeff1oleme  13446  tangtx  13512  cosordlem  13523  logdivlti  13555  apcxp2  13611  lgsdilem  13681  2sqlem3  13706  2sqlem8  13712  apdifflemr  14039