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  6034  caovcand  6037  caovordid  6041  caovordd  6043  caovdid  6050  caovdird  6053  swoer  6563  swoord1  6564  swoord2  6565  fimax2gtrilemstep  6900  iunfidisj  6945  ssfii  6973  suplub2ti  7000  prarloclem3  7496  fzosubel3  10196  seq3split  10479  seq3caopr  10483  zsumdc  11392  fsumiun  11485  divalglemex  11927  pcgcd1  12327  strle1g  12565  mnd32g  12828  mnd12g  12829  mnd4g  12830  ismndd  12838  mndinvmod  12846  grpasscan2  12934  grpidrcan  12935  grpidlcan  12936  grpinvinv  12937  grplmulf1o  12944  grpinvssd  12947  grpinvadd  12948  grpsubrcan  12951  grpsubadd  12958  grpaddsubass  12960  grppncan  12961  grpsubsub4  12963  grppnpcan2  12964  grpnpncan  12965  grpnpncan0  12966  grpnnncan2  12967  dfgrp3mlem  12968  dfgrp3m  12969  grplactcnv  12972  mhmmnd  12980  mulgaddcomlem  13006  mulgaddcom  13007  mulgnn0dir  13013  mulgdirlem  13014  mulgneg2  13017  mulgnnass  13018  mulgnn0ass  13019  mulgass  13020  mulgmodid  13022  nsgconj  13066  isnsg3  13067  nmzsubg  13070  ssnmz  13071  eqger  13083  eqgcpbl  13087  abl32  13110  abladdsub4  13117  abladdsub  13118  ablpncan2  13119  ablsubsub  13121  srgass  13154  srgmulgass  13172  srgpcomp  13173  srgpcompp  13174  srgpcomppsc  13175  ringass  13199  ringadd2  13210  ringo2times  13211  ringcom  13214  ringlz  13222  ringrz  13223  ringnegl  13228  ringnegr  13229  ringmneg1  13230  ringmneg2  13231  ringsubdi  13233  ringsubdir  13234  mulgass2  13235  opprring  13249  mulgass3  13254  dvdsrtr  13270  dvdsrmul1  13271  unitgrp  13285  dvrass  13308  dvrcan1  13309  dvrcan3  13310  dvrdir  13312  rdivmuldivd  13313  lringuplu  13337  subrginv  13358  aprcotr  13375  islmod  13381  lmod0vs  13411  lmodvs0  13412  lmodvsmmulgdi  13413  lmodfopne  13416  lmodvneg1  13420  lmodvsneg  13421  lmodcom  13423  lmodsubvs  13433  lmodsubdi  13434  lmodsubdir  13435  psmetsym  13832  psmettri  13833  psmetge0  13834  psmetres2  13836  xmetge0  13868  xmetsym  13871  xmettri  13875  metrtri  13880  xmetres2  13882  bldisj  13904  xblss2ps  13907  xblss2  13908  xmeter  13939  xmetxp  14010