Theorem syl13anc 1280

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 1208	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
6		syl13anc.5	. 2 |- ( ( ps /\ ( ch /\ th /\ ta ) ) -> et )
7	1, 5, 6	syl2anc 415	1 |- ( ph -> et )

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

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 1011

This theorem is referenced by:  syl23anc  1285  syl33anc  1293  caovassd  6239  caovcand  6242  caovordid  6246  caovordd  6248  caovdid  6255  caovdird  6258  swoer  6825  swoord1  6826  swoord2  6827  fimax2gtrilemstep  7195  iunfidisj  7250  ssfii  7298  suplub2ti  7331  prarloclem3  7854  fzosubel3  10592  seq3split  10903  seqsplitg  10904  seq3caopr  10910  seqcaoprg  10911  zsumdc  12129  fsumiun  12222  divalglemex  12667  pcgcd1  13085  strle1g  13437  mnd32g  13717  mnd12g  13718  mnd4g  13719  ismndd  13727  mndinvmod  13735  imasmnd  13737  grpassd  13794  grpasscan2  13846  grpidrcan  13847  grpidlcan  13848  grpinvinv  13849  grplmulf1o  13856  grpinvssd  13859  grpinvadd  13860  grpsubrcan  13863  grpsubadd  13870  grpaddsubass  13872  grppncan  13873  grpsubsub4  13875  grppnpcan2  13876  grpnpncan  13877  grpnpncan0  13878  grpnnncan2  13879  dfgrp3mlem  13880  dfgrp3m  13881  grplactcnv  13884  imasgrp  13891  mhmmnd  13896  mulgaddcomlem  13925  mulgaddcom  13926  mulgnn0dir  13932  mulgdirlem  13933  mulgneg2  13936  mulgnnass  13937  mulgnn0ass  13938  mulgass  13939  mulgmodid  13941  nsgconj  13986  isnsg3  13987  nmzsubg  13990  ssnmz  13991  eqger  14004  eqgcpbl  14008  conjghm  14056  conjnmz  14059  conjnmzb  14060  abl32  14087  abladdsub4  14095  abladdsub  14096  ablpncan2  14097  ablsubsub  14099  prdssgrpd  14168  prdsmndd  14171  rngass  14213  rnglz  14219  rngrz  14220  rngmneg1  14221  rngmneg2  14222  rngsubdi  14225  rngsubdir  14226  imasrng  14230  srgass  14249  srgmulgass  14267  srgpcomp  14268  srgpcompp  14269  srgpcomppsc  14270  ringass  14294  ringadd2  14305  ringo2times  14306  ringcom  14309  ringlz  14321  ringrz  14322  ringnegl  14329  ringnegr  14330  ringmneg1  14331  ringmneg2  14332  ringsubdi  14334  ringsubdir  14335  mulgass2  14336  imasring  14342  opprrng  14355  opprring  14357  mulgass3  14364  dvdsrtr  14381  dvdsrmul1  14382  unitgrp  14396  dvrass  14419  dvrcan1  14420  dvrcan3  14421  dvrdir  14423  rdivmuldivd  14424  rhmunitinv  14458  lringuplu  14476  subrginv  14518  unitrrg  14549  aprcotr  14570  islmod  14600  lmod0vs  14630  lmodvs0  14631  lmodvsmmulgdi  14632  lmodfopne  14635  lmodvneg1  14639  lmodvsneg  14640  lmodcom  14642  lmodsubvs  14652  lmodsubdi  14653  lmodsubdir  14654  islss3  14688  lss1d  14692  sralmod  14759  rnglidlmsgrp  14806  2idlcpblrng  14832  mulgrhm  14916  psmetsym  15353  psmettri  15354  psmetge0  15355  psmetres2  15357  xmetge0  15389  xmetsym  15392  xmettri  15396  metrtri  15401  xmetres2  15403  bldisj  15425  xblss2ps  15428  xblss2  15429  xmeter  15460  xmetxp  15531  dvdsppwf1o  16017  perfect1  16026  perfectlem1  16027  perfectlem2  16028  3dom  16932