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  6839  swoord1  6840  swoord2  6841  fimax2gtrilemstep  7209  iunfidisj  7264  ssfii  7313  suplub2ti  7347  prarloclem3  7870  fzosubel3  10631  seq3split  10946  seqsplitg  10947  seq3caopr  10953  seqcaoprg  10954  zsumdc  12176  fsumiun  12269  divalglemex  12714  pcgcd1  13136  strle1g  13519  mnd32g  13799  mnd12g  13800  mnd4g  13801  ismndd  13809  mndinvmod  13817  imasmnd  13819  grpassd  13876  grpasscan2  13928  grpidrcan  13929  grpidlcan  13930  grpinvinv  13931  grplmulf1o  13938  grpinvssd  13941  grpinvadd  13942  grpsubrcan  13945  grpsubadd  13952  grpaddsubass  13954  grppncan  13955  grpsubsub4  13957  grppnpcan2  13958  grpnpncan  13959  grpnpncan0  13960  grpnnncan2  13961  dfgrp3mlem  13962  dfgrp3m  13963  grplactcnv  13966  imasgrp  13973  mhmmnd  13978  mulgaddcomlem  14007  mulgaddcom  14008  mulgnn0dir  14014  mulgdirlem  14015  mulgneg2  14018  mulgnnass  14019  mulgnn0ass  14020  mulgass  14021  mulgmodid  14023  nsgconj  14068  isnsg3  14069  nmzsubg  14072  ssnmz  14073  eqger  14086  eqgcpbl  14090  conjghm  14138  conjnmz  14141  conjnmzb  14142  cntzsgrpcl  14167  cntzsubm  14170  cntzsubg  14171  abl32  14200  abladdsub4  14208  abladdsub  14209  ablpncan2  14210  ablsubsub  14212  gsummptfidmsplit  14254  prdssgrpd  14298  prdsmndd  14301  rngass  14345  rnglz  14351  rngrz  14352  rngmneg1  14353  rngmneg2  14354  rngsubdi  14357  rngsubdir  14358  imasrng  14362  srgass  14382  srgmulgass  14400  srgpcomp  14401  srgpcompp  14402  srgpcomppsc  14403  ringass  14427  ringadd2  14439  ringo2times  14440  ringcom  14443  ringlz  14455  ringrz  14456  ringnegl  14463  ringnegr  14464  ringmneg1  14465  ringmneg2  14466  ringsubdi  14468  ringsubdir  14469  mulgass2  14470  imasring  14478  opprrng  14491  opprring  14493  mulgass3  14500  dvdsrtr  14517  dvdsrmul1  14518  unitgrp  14532  dvrass  14555  dvrcan1  14556  dvrcan3  14557  dvrdir  14559  rdivmuldivd  14560  rhmunitinv  14594  lringuplu  14612  subrginv  14654  unitrrg  14685  aprcotr  14706  islmod  14736  lmod0vs  14767  lmodvs0  14768  lmodvsmmulgdi  14769  lmodfopne  14772  lmodvneg1  14776  lmodvsneg  14777  lmodcom  14779  lmodsubvs  14789  lmodsubdi  14790  lmodsubdir  14791  islss3  14825  lss1d  14829  sralmod  14896  rnglidlmsgrp  14943  2idlcpblrng  14969  mulgrhm  15053  assa2ass  15118  assa2ass2  15119  asclghm  15134  asclmul1  15138  asclmul2  15139  ascldimul  15140  assamulgscmlem2  15151  asclmulg  15153  psrass1fi  15201  psrdifi  15202  psrdirfi  15203  psmetsym  15555  psmettri  15556  psmetge0  15557  psmetres2  15559  xmetge0  15591  xmetsym  15594  xmettri  15598  metrtri  15603  xmetres2  15605  bldisj  15627  xblss2ps  15630  xblss2  15631  xmeter  15662  xmetxp  15733  dvdsppwf1o  16283  perfect1  16298  perfectlem1  16299  perfectlem2  16300  3dom  17223