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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl23anc  1285  syl33anc  1293  caovassd  6252  caovcand  6255  caovordid  6259  caovordd  6261  caovdid  6268  caovdird  6271  swoer  6840  swoord1  6841  swoord2  6842  fimax2gtrilemstep  7211  iunfidisj  7266  ssfii  7313  suplub2ti  7347  prarloclem3  7870  fzosubel3  10630  seq3split  10945  seqsplitg  10946  seq3caopr  10952  seqcaoprg  10953  zsumdc  12175  fsumiun  12268  divalglemex  12713  pcgcd1  13135  strle1g  13518  mnd32g  13798  mnd12g  13799  mnd4g  13800  ismndd  13808  mndinvmod  13816  imasmnd  13818  grpassd  13875  grpasscan2  13927  grpidrcan  13928  grpidlcan  13929  grpinvinv  13930  grplmulf1o  13937  grpinvssd  13940  grpinvadd  13941  grpsubrcan  13944  grpsubadd  13951  grpaddsubass  13953  grppncan  13954  grpsubsub4  13956  grppnpcan2  13957  grpnpncan  13958  grpnpncan0  13959  grpnnncan2  13960  dfgrp3mlem  13961  dfgrp3m  13962  grplactcnv  13965  imasgrp  13972  mhmmnd  13977  mulgaddcomlem  14006  mulgaddcom  14007  mulgnn0dir  14013  mulgdirlem  14014  mulgneg2  14017  mulgnnass  14018  mulgnn0ass  14019  mulgass  14020  mulgmodid  14022  nsgconj  14067  isnsg3  14068  nmzsubg  14071  ssnmz  14072  eqger  14085  eqgcpbl  14089  conjghm  14137  conjnmz  14140  conjnmzb  14141  cntzsgrpcl  14166  cntzsubm  14169  cntzsubg  14170  abl32  14199  abladdsub4  14207  abladdsub  14208  ablpncan2  14209  ablsubsub  14211  gsummptfidmsplit  14253  prdssgrpd  14297  prdsmndd  14300  rngass  14344  rnglz  14350  rngrz  14351  rngmneg1  14352  rngmneg2  14353  rngsubdi  14356  rngsubdir  14357  imasrng  14361  srgass  14381  srgmulgass  14399  srgpcomp  14400  srgpcompp  14401  srgpcomppsc  14402  ringass  14426  ringadd2  14438  ringo2times  14439  ringcom  14442  ringlz  14454  ringrz  14455  ringnegl  14462  ringnegr  14463  ringmneg1  14464  ringmneg2  14465  ringsubdi  14467  ringsubdir  14468  mulgass2  14469  imasring  14477  opprrng  14490  opprring  14492  mulgass3  14499  dvdsrtr  14516  dvdsrmul1  14517  unitgrp  14531  dvrass  14554  dvrcan1  14555  dvrcan3  14556  dvrdir  14558  rdivmuldivd  14559  rhmunitinv  14593  lringuplu  14611  subrginv  14653  unitrrg  14684  aprcotr  14705  islmod  14735  lmod0vs  14766  lmodvs0  14767  lmodvsmmulgdi  14768  lmodfopne  14771  lmodvneg1  14775  lmodvsneg  14776  lmodcom  14778  lmodsubvs  14788  lmodsubdi  14789  lmodsubdir  14790  islss3  14824  lss1d  14828  sralmod  14895  rnglidlmsgrp  14942  2idlcpblrng  14968  mulgrhm  15052  assa2ass  15117  assa2ass2  15118  asclghm  15133  asclmul1  15137  asclmul2  15138  ascldimul  15139  assamulgscmlem2  15150  asclmulg  15152  psrass1fi  15210  psrdifi  15211  psrdirfi  15212  psmetsym  15572  psmettri  15573  psmetge0  15574  psmetres2  15576  xmetge0  15608  xmetsym  15611  xmettri  15615  metrtri  15620  xmetres2  15622  bldisj  15644  xblss2ps  15647  xblss2  15648  xmeter  15679  xmetxp  15750  dvdsppwf1o  16300  perfect1  16315  perfectlem1  16316  perfectlem2  16317  3dom  17240