Theorem syl13anc 1240

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 )
syl13anc.5	|- ( ( ps /\ ( ch /\ th /\ ta ) ) -> et )

Assertion

Ref	Expression
syl13anc	|- ( ph -> et )

Proof of Theorem syl13anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4		sylXanc.4	. . 3 |- ( ph -> ta )
5	2, 3, 4	3jca 1177	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
6		syl13anc.5	. 2 |- ( ( ps /\ ( ch /\ th /\ ta ) ) -> et )
7	1, 5, 6	syl2anc 411	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

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 980

This theorem is referenced by:  syl23anc  1245  syl33anc  1253  caovassd  6024  caovcand  6027  caovordid  6031  caovordd  6033  caovdid  6040  caovdird  6043  swoer  6553  swoord1  6554  swoord2  6555  fimax2gtrilemstep  6890  iunfidisj  6935  ssfii  6963  suplub2ti  6990  prarloclem3  7471  fzosubel3  10164  seq3split  10447  seq3caopr  10451  zsumdc  11358  fsumiun  11451  divalglemex  11892  pcgcd1  12292  strle1g  12519  mnd32g  12692  mnd12g  12693  mnd4g  12694  ismndd  12702  mndinvmod  12707  grpasscan2  12793  grpidrcan  12794  grpidlcan  12795  grpinvinv  12796  grplmulf1o  12803  grpinvssd  12806  grpinvadd  12807  grpsubrcan  12810  grpsubadd  12817  grpaddsubass  12819  grppncan  12820  grpsubsub4  12822  grppnpcan2  12823  grpnpncan  12824  grpnpncan0  12825  grpnnncan2  12826  dfgrp3mlem  12827  dfgrp3m  12828  grplactcnv  12831  mhmmnd  12839  mulgaddcomlem  12864  mulgaddcom  12865  mulgnn0dir  12871  mulgdirlem  12872  mulgneg2  12875  mulgnnass  12876  mulgnn0ass  12877  mulgass  12878  mulgmodid  12880  abl32  12906  abladdsub4  12913  abladdsub  12914  ablpncan2  12915  ablsubsub  12917  srgass  12947  srgmulgass  12965  srgpcomp  12966  srgpcompp  12967  srgpcomppsc  12968  ringass  12992  ringadd2  13003  rngo2times  13004  ringcom  13006  ringlz  13014  ringrz  13015  ringnegl  13020  rngnegr  13021  ringmneg1  13022  ringmneg2  13023  ringsubdi  13025  rngsubdir  13026  mulgass2  13027  psmetsym  13380  psmettri  13381  psmetge0  13382  psmetres2  13384  xmetge0  13416  xmetsym  13419  xmettri  13423  metrtri  13428  xmetres2  13430  bldisj  13452  xblss2ps  13455  xblss2  13456  xmeter  13487  xmetxp  13558