Theorem syl13anc 1276

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 1204	. 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 1005

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 1007

This theorem is referenced by:  syl23anc  1281  syl33anc  1289  caovassd  6192  caovcand  6195  caovordid  6199  caovordd  6201  caovdid  6208  caovdird  6211  swoer  6773  swoord1  6774  swoord2  6775  fimax2gtrilemstep  7133  iunfidisj  7188  ssfii  7216  suplub2ti  7243  prarloclem3  7760  fzosubel3  10487  seq3split  10796  seqsplitg  10797  seq3caopr  10803  seqcaoprg  10804  zsumdc  12008  fsumiun  12101  divalglemex  12546  pcgcd1  12964  strle1g  13252  prdssgrpd  13561  mnd32g  13573  mnd12g  13574  mnd4g  13575  ismndd  13583  mndinvmod  13591  prdsmndd  13594  imasmnd  13599  grpassd  13658  grpasscan2  13710  grpidrcan  13711  grpidlcan  13712  grpinvinv  13713  grplmulf1o  13720  grpinvssd  13723  grpinvadd  13724  grpsubrcan  13727  grpsubadd  13734  grpaddsubass  13736  grppncan  13737  grpsubsub4  13739  grppnpcan2  13740  grpnpncan  13741  grpnpncan0  13742  grpnnncan2  13743  dfgrp3mlem  13744  dfgrp3m  13745  grplactcnv  13748  imasgrp  13761  mhmmnd  13766  mulgaddcomlem  13795  mulgaddcom  13796  mulgnn0dir  13802  mulgdirlem  13803  mulgneg2  13806  mulgnnass  13807  mulgnn0ass  13808  mulgass  13809  mulgmodid  13811  nsgconj  13856  isnsg3  13857  nmzsubg  13860  ssnmz  13861  eqger  13874  eqgcpbl  13878  conjghm  13926  conjnmz  13929  conjnmzb  13930  abl32  13957  abladdsub4  13964  abladdsub  13965  ablpncan2  13966  ablsubsub  13968  rngass  14016  rnglz  14022  rngrz  14023  rngmneg1  14024  rngmneg2  14025  rngsubdi  14028  rngsubdir  14029  imasrng  14033  srgass  14048  srgmulgass  14066  srgpcomp  14067  srgpcompp  14068  srgpcomppsc  14069  ringass  14093  ringadd2  14104  ringo2times  14105  ringcom  14108  ringlz  14120  ringrz  14121  ringnegl  14128  ringnegr  14129  ringmneg1  14130  ringmneg2  14131  ringsubdi  14133  ringsubdir  14134  mulgass2  14135  imasring  14141  opprrng  14154  opprring  14156  mulgass3  14162  dvdsrtr  14179  dvdsrmul1  14180  unitgrp  14194  dvrass  14217  dvrcan1  14218  dvrcan3  14219  dvrdir  14221  rdivmuldivd  14222  rhmunitinv  14256  lringuplu  14274  subrginv  14315  unitrrg  14346  aprcotr  14364  islmod  14370  lmod0vs  14400  lmodvs0  14401  lmodvsmmulgdi  14402  lmodfopne  14405  lmodvneg1  14409  lmodvsneg  14410  lmodcom  14412  lmodsubvs  14422  lmodsubdi  14423  lmodsubdir  14424  islss3  14458  lss1d  14462  sralmod  14529  rnglidlmsgrp  14576  2idlcpblrng  14602  mulgrhm  14688  psmetsym  15123  psmettri  15124  psmetge0  15125  psmetres2  15127  xmetge0  15159  xmetsym  15162  xmettri  15166  metrtri  15171  xmetres2  15173  bldisj  15195  xblss2ps  15198  xblss2  15199  xmeter  15230  xmetxp  15301  dvdsppwf1o  15786  perfect1  15795  perfectlem1  15796  perfectlem2  15797  3dom  16691