Theorem syl13anc 1275

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 1203	. 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 1004

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 1006

This theorem is referenced by:  syl23anc  1280  syl33anc  1288  caovassd  6181  caovcand  6184  caovordid  6188  caovordd  6190  caovdid  6197  caovdird  6200  swoer  6729  swoord1  6730  swoord2  6731  fimax2gtrilemstep  7089  iunfidisj  7144  ssfii  7172  suplub2ti  7199  prarloclem3  7716  fzosubel3  10440  seq3split  10749  seqsplitg  10750  seq3caopr  10756  seqcaoprg  10757  zsumdc  11944  fsumiun  12037  divalglemex  12482  pcgcd1  12900  strle1g  13188  prdssgrpd  13497  mnd32g  13509  mnd12g  13510  mnd4g  13511  ismndd  13519  mndinvmod  13527  prdsmndd  13530  imasmnd  13535  grpassd  13594  grpasscan2  13646  grpidrcan  13647  grpidlcan  13648  grpinvinv  13649  grplmulf1o  13656  grpinvssd  13659  grpinvadd  13660  grpsubrcan  13663  grpsubadd  13670  grpaddsubass  13672  grppncan  13673  grpsubsub4  13675  grppnpcan2  13676  grpnpncan  13677  grpnpncan0  13678  grpnnncan2  13679  dfgrp3mlem  13680  dfgrp3m  13681  grplactcnv  13684  imasgrp  13697  mhmmnd  13702  mulgaddcomlem  13731  mulgaddcom  13732  mulgnn0dir  13738  mulgdirlem  13739  mulgneg2  13742  mulgnnass  13743  mulgnn0ass  13744  mulgass  13745  mulgmodid  13747  nsgconj  13792  isnsg3  13793  nmzsubg  13796  ssnmz  13797  eqger  13810  eqgcpbl  13814  conjghm  13862  conjnmz  13865  conjnmzb  13866  abl32  13893  abladdsub4  13900  abladdsub  13901  ablpncan2  13902  ablsubsub  13904  rngass  13951  rnglz  13957  rngrz  13958  rngmneg1  13959  rngmneg2  13960  rngsubdi  13963  rngsubdir  13964  imasrng  13968  srgass  13983  srgmulgass  14001  srgpcomp  14002  srgpcompp  14003  srgpcomppsc  14004  ringass  14028  ringadd2  14039  ringo2times  14040  ringcom  14043  ringlz  14055  ringrz  14056  ringnegl  14063  ringnegr  14064  ringmneg1  14065  ringmneg2  14066  ringsubdi  14068  ringsubdir  14069  mulgass2  14070  imasring  14076  opprrng  14089  opprring  14091  mulgass3  14097  dvdsrtr  14114  dvdsrmul1  14115  unitgrp  14129  dvrass  14152  dvrcan1  14153  dvrcan3  14154  dvrdir  14156  rdivmuldivd  14157  rhmunitinv  14191  lringuplu  14209  subrginv  14250  unitrrg  14280  aprcotr  14298  islmod  14304  lmod0vs  14334  lmodvs0  14335  lmodvsmmulgdi  14336  lmodfopne  14339  lmodvneg1  14343  lmodvsneg  14344  lmodcom  14346  lmodsubvs  14356  lmodsubdi  14357  lmodsubdir  14358  islss3  14392  lss1d  14396  sralmod  14463  rnglidlmsgrp  14510  2idlcpblrng  14536  mulgrhm  14622  psmetsym  15052  psmettri  15053  psmetge0  15054  psmetres2  15056  xmetge0  15088  xmetsym  15091  xmettri  15095  metrtri  15100  xmetres2  15102  bldisj  15124  xblss2ps  15127  xblss2  15128  xmeter  15159  xmetxp  15230  dvdsppwf1o  15712  perfect1  15721  perfectlem1  15722  perfectlem2  15723  3dom  16587