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  6164  caovcand  6167  caovordid  6171  caovordd  6173  caovdid  6180  caovdird  6183  swoer  6706  swoord1  6707  swoord2  6708  fimax2gtrilemstep  7058  iunfidisj  7109  ssfii  7137  suplub2ti  7164  prarloclem3  7680  fzosubel3  10397  seq3split  10705  seqsplitg  10706  seq3caopr  10712  seqcaoprg  10713  zsumdc  11890  fsumiun  11983  divalglemex  12428  pcgcd1  12846  strle1g  13134  prdssgrpd  13443  mnd32g  13455  mnd12g  13456  mnd4g  13457  ismndd  13465  mndinvmod  13473  prdsmndd  13476  imasmnd  13481  grpassd  13540  grpasscan2  13592  grpidrcan  13593  grpidlcan  13594  grpinvinv  13595  grplmulf1o  13602  grpinvssd  13605  grpinvadd  13606  grpsubrcan  13609  grpsubadd  13616  grpaddsubass  13618  grppncan  13619  grpsubsub4  13621  grppnpcan2  13622  grpnpncan  13623  grpnpncan0  13624  grpnnncan2  13625  dfgrp3mlem  13626  dfgrp3m  13627  grplactcnv  13630  imasgrp  13643  mhmmnd  13648  mulgaddcomlem  13677  mulgaddcom  13678  mulgnn0dir  13684  mulgdirlem  13685  mulgneg2  13688  mulgnnass  13689  mulgnn0ass  13690  mulgass  13691  mulgmodid  13693  nsgconj  13738  isnsg3  13739  nmzsubg  13742  ssnmz  13743  eqger  13756  eqgcpbl  13760  conjghm  13808  conjnmz  13811  conjnmzb  13812  abl32  13839  abladdsub4  13846  abladdsub  13847  ablpncan2  13848  ablsubsub  13850  rngass  13897  rnglz  13903  rngrz  13904  rngmneg1  13905  rngmneg2  13906  rngsubdi  13909  rngsubdir  13910  imasrng  13914  srgass  13929  srgmulgass  13947  srgpcomp  13948  srgpcompp  13949  srgpcomppsc  13950  ringass  13974  ringadd2  13985  ringo2times  13986  ringcom  13989  ringlz  14001  ringrz  14002  ringnegl  14009  ringnegr  14010  ringmneg1  14011  ringmneg2  14012  ringsubdi  14014  ringsubdir  14015  mulgass2  14016  imasring  14022  opprrng  14035  opprring  14037  mulgass3  14043  dvdsrtr  14059  dvdsrmul1  14060  unitgrp  14074  dvrass  14097  dvrcan1  14098  dvrcan3  14099  dvrdir  14101  rdivmuldivd  14102  rhmunitinv  14136  lringuplu  14154  subrginv  14195  unitrrg  14225  aprcotr  14243  islmod  14249  lmod0vs  14279  lmodvs0  14280  lmodvsmmulgdi  14281  lmodfopne  14284  lmodvneg1  14288  lmodvsneg  14289  lmodcom  14291  lmodsubvs  14301  lmodsubdi  14302  lmodsubdir  14303  islss3  14337  lss1d  14341  sralmod  14408  rnglidlmsgrp  14455  2idlcpblrng  14481  mulgrhm  14567  psmetsym  14997  psmettri  14998  psmetge0  14999  psmetres2  15001  xmetge0  15033  xmetsym  15036  xmettri  15040  metrtri  15045  xmetres2  15047  bldisj  15069  xblss2ps  15072  xblss2  15073  xmeter  15104  xmetxp  15175  dvdsppwf1o  15657  perfect1  15666  perfectlem1  15667  perfectlem2  15668