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  6214  caovcand  6217  caovordid  6221  caovordd  6223  caovdid  6230  caovdird  6233  swoer  6795  swoord1  6796  swoord2  6797  fimax2gtrilemstep  7158  iunfidisj  7213  ssfii  7261  suplub2ti  7292  prarloclem3  7812  fzosubel3  10541  seq3split  10850  seqsplitg  10851  seq3caopr  10857  seqcaoprg  10858  zsumdc  12070  fsumiun  12163  divalglemex  12608  pcgcd1  13026  strle1g  13319  prdssgrpd  13628  mnd32g  13640  mnd12g  13641  mnd4g  13642  ismndd  13650  mndinvmod  13658  prdsmndd  13661  imasmnd  13666  grpassd  13725  grpasscan2  13777  grpidrcan  13778  grpidlcan  13779  grpinvinv  13780  grplmulf1o  13787  grpinvssd  13790  grpinvadd  13791  grpsubrcan  13794  grpsubadd  13801  grpaddsubass  13803  grppncan  13804  grpsubsub4  13806  grppnpcan2  13807  grpnpncan  13808  grpnpncan0  13809  grpnnncan2  13810  dfgrp3mlem  13811  dfgrp3m  13812  grplactcnv  13815  imasgrp  13828  mhmmnd  13833  mulgaddcomlem  13862  mulgaddcom  13863  mulgnn0dir  13869  mulgdirlem  13870  mulgneg2  13873  mulgnnass  13874  mulgnn0ass  13875  mulgass  13876  mulgmodid  13878  nsgconj  13923  isnsg3  13924  nmzsubg  13927  ssnmz  13928  eqger  13941  eqgcpbl  13945  conjghm  13993  conjnmz  13996  conjnmzb  13997  abl32  14024  abladdsub4  14031  abladdsub  14032  ablpncan2  14033  ablsubsub  14035  rngass  14083  rnglz  14089  rngrz  14090  rngmneg1  14091  rngmneg2  14092  rngsubdi  14095  rngsubdir  14096  imasrng  14100  srgass  14115  srgmulgass  14133  srgpcomp  14134  srgpcompp  14135  srgpcomppsc  14136  ringass  14160  ringadd2  14171  ringo2times  14172  ringcom  14175  ringlz  14187  ringrz  14188  ringnegl  14195  ringnegr  14196  ringmneg1  14197  ringmneg2  14198  ringsubdi  14200  ringsubdir  14201  mulgass2  14202  imasring  14208  opprrng  14221  opprring  14223  mulgass3  14229  dvdsrtr  14246  dvdsrmul1  14247  unitgrp  14261  dvrass  14284  dvrcan1  14285  dvrcan3  14286  dvrdir  14288  rdivmuldivd  14289  rhmunitinv  14323  lringuplu  14341  subrginv  14382  unitrrg  14413  aprcotr  14431  islmod  14439  lmod0vs  14469  lmodvs0  14470  lmodvsmmulgdi  14471  lmodfopne  14474  lmodvneg1  14478  lmodvsneg  14479  lmodcom  14481  lmodsubvs  14491  lmodsubdi  14492  lmodsubdir  14493  islss3  14527  lss1d  14531  sralmod  14598  rnglidlmsgrp  14645  2idlcpblrng  14671  mulgrhm  14757  psmetsym  15194  psmettri  15195  psmetge0  15196  psmetres2  15198  xmetge0  15230  xmetsym  15233  xmettri  15237  metrtri  15242  xmetres2  15244  bldisj  15266  xblss2ps  15269  xblss2  15270  xmeter  15301  xmetxp  15372  dvdsppwf1o  15857  perfect1  15866  perfectlem1  15867  perfectlem2  15868  3dom  16762