Theorem syl13anc 1273

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 1201	. 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 1002

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 1004

This theorem is referenced by:  syl23anc  1278  syl33anc  1286  caovassd  6177  caovcand  6180  caovordid  6184  caovordd  6186  caovdid  6193  caovdird  6196  swoer  6725  swoord1  6726  swoord2  6727  fimax2gtrilemstep  7083  iunfidisj  7136  ssfii  7164  suplub2ti  7191  prarloclem3  7707  fzosubel3  10431  seq3split  10740  seqsplitg  10741  seq3caopr  10747  seqcaoprg  10748  zsumdc  11935  fsumiun  12028  divalglemex  12473  pcgcd1  12891  strle1g  13179  prdssgrpd  13488  mnd32g  13500  mnd12g  13501  mnd4g  13502  ismndd  13510  mndinvmod  13518  prdsmndd  13521  imasmnd  13526  grpassd  13585  grpasscan2  13637  grpidrcan  13638  grpidlcan  13639  grpinvinv  13640  grplmulf1o  13647  grpinvssd  13650  grpinvadd  13651  grpsubrcan  13654  grpsubadd  13661  grpaddsubass  13663  grppncan  13664  grpsubsub4  13666  grppnpcan2  13667  grpnpncan  13668  grpnpncan0  13669  grpnnncan2  13670  dfgrp3mlem  13671  dfgrp3m  13672  grplactcnv  13675  imasgrp  13688  mhmmnd  13693  mulgaddcomlem  13722  mulgaddcom  13723  mulgnn0dir  13729  mulgdirlem  13730  mulgneg2  13733  mulgnnass  13734  mulgnn0ass  13735  mulgass  13736  mulgmodid  13738  nsgconj  13783  isnsg3  13784  nmzsubg  13787  ssnmz  13788  eqger  13801  eqgcpbl  13805  conjghm  13853  conjnmz  13856  conjnmzb  13857  abl32  13884  abladdsub4  13891  abladdsub  13892  ablpncan2  13893  ablsubsub  13895  rngass  13942  rnglz  13948  rngrz  13949  rngmneg1  13950  rngmneg2  13951  rngsubdi  13954  rngsubdir  13955  imasrng  13959  srgass  13974  srgmulgass  13992  srgpcomp  13993  srgpcompp  13994  srgpcomppsc  13995  ringass  14019  ringadd2  14030  ringo2times  14031  ringcom  14034  ringlz  14046  ringrz  14047  ringnegl  14054  ringnegr  14055  ringmneg1  14056  ringmneg2  14057  ringsubdi  14059  ringsubdir  14060  mulgass2  14061  imasring  14067  opprrng  14080  opprring  14082  mulgass3  14088  dvdsrtr  14105  dvdsrmul1  14106  unitgrp  14120  dvrass  14143  dvrcan1  14144  dvrcan3  14145  dvrdir  14147  rdivmuldivd  14148  rhmunitinv  14182  lringuplu  14200  subrginv  14241  unitrrg  14271  aprcotr  14289  islmod  14295  lmod0vs  14325  lmodvs0  14326  lmodvsmmulgdi  14327  lmodfopne  14330  lmodvneg1  14334  lmodvsneg  14335  lmodcom  14337  lmodsubvs  14347  lmodsubdi  14348  lmodsubdir  14349  islss3  14383  lss1d  14387  sralmod  14454  rnglidlmsgrp  14501  2idlcpblrng  14527  mulgrhm  14613  psmetsym  15043  psmettri  15044  psmetge0  15045  psmetres2  15047  xmetge0  15079  xmetsym  15082  xmettri  15086  metrtri  15091  xmetres2  15093  bldisj  15115  xblss2ps  15118  xblss2  15119  xmeter  15150  xmetxp  15221  dvdsppwf1o  15703  perfect1  15712  perfectlem1  15713  perfectlem2  15714  3dom  16523