Theorem syl13anc 1275

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 1203	. 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 1004

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 1006

This theorem is referenced by:  syl23anc  1280  syl33anc  1288  caovassd  6182  caovcand  6185  caovordid  6189  caovordd  6191  caovdid  6198  caovdird  6201  swoer  6730  swoord1  6731  swoord2  6732  fimax2gtrilemstep  7090  iunfidisj  7145  ssfii  7173  suplub2ti  7200  prarloclem3  7717  fzosubel3  10442  seq3split  10751  seqsplitg  10752  seq3caopr  10758  seqcaoprg  10759  zsumdc  11963  fsumiun  12056  divalglemex  12501  pcgcd1  12919  strle1g  13207  prdssgrpd  13516  mnd32g  13528  mnd12g  13529  mnd4g  13530  ismndd  13538  mndinvmod  13546  prdsmndd  13549  imasmnd  13554  grpassd  13613  grpasscan2  13665  grpidrcan  13666  grpidlcan  13667  grpinvinv  13668  grplmulf1o  13675  grpinvssd  13678  grpinvadd  13679  grpsubrcan  13682  grpsubadd  13689  grpaddsubass  13691  grppncan  13692  grpsubsub4  13694  grppnpcan2  13695  grpnpncan  13696  grpnpncan0  13697  grpnnncan2  13698  dfgrp3mlem  13699  dfgrp3m  13700  grplactcnv  13703  imasgrp  13716  mhmmnd  13721  mulgaddcomlem  13750  mulgaddcom  13751  mulgnn0dir  13757  mulgdirlem  13758  mulgneg2  13761  mulgnnass  13762  mulgnn0ass  13763  mulgass  13764  mulgmodid  13766  nsgconj  13811  isnsg3  13812  nmzsubg  13815  ssnmz  13816  eqger  13829  eqgcpbl  13833  conjghm  13881  conjnmz  13884  conjnmzb  13885  abl32  13912  abladdsub4  13919  abladdsub  13920  ablpncan2  13921  ablsubsub  13923  rngass  13971  rnglz  13977  rngrz  13978  rngmneg1  13979  rngmneg2  13980  rngsubdi  13983  rngsubdir  13984  imasrng  13988  srgass  14003  srgmulgass  14021  srgpcomp  14022  srgpcompp  14023  srgpcomppsc  14024  ringass  14048  ringadd2  14059  ringo2times  14060  ringcom  14063  ringlz  14075  ringrz  14076  ringnegl  14083  ringnegr  14084  ringmneg1  14085  ringmneg2  14086  ringsubdi  14088  ringsubdir  14089  mulgass2  14090  imasring  14096  opprrng  14109  opprring  14111  mulgass3  14117  dvdsrtr  14134  dvdsrmul1  14135  unitgrp  14149  dvrass  14172  dvrcan1  14173  dvrcan3  14174  dvrdir  14176  rdivmuldivd  14177  rhmunitinv  14211  lringuplu  14229  subrginv  14270  unitrrg  14300  aprcotr  14318  islmod  14324  lmod0vs  14354  lmodvs0  14355  lmodvsmmulgdi  14356  lmodfopne  14359  lmodvneg1  14363  lmodvsneg  14364  lmodcom  14366  lmodsubvs  14376  lmodsubdi  14377  lmodsubdir  14378  islss3  14412  lss1d  14416  sralmod  14483  rnglidlmsgrp  14530  2idlcpblrng  14556  mulgrhm  14642  psmetsym  15072  psmettri  15073  psmetge0  15074  psmetres2  15076  xmetge0  15108  xmetsym  15111  xmettri  15115  metrtri  15120  xmetres2  15122  bldisj  15144  xblss2ps  15147  xblss2  15148  xmeter  15179  xmetxp  15250  dvdsppwf1o  15732  perfect1  15741  perfectlem1  15742  perfectlem2  15743  3dom  16638