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  6171  caovcand  6174  caovordid  6178  caovordd  6180  caovdid  6187  caovdird  6190  swoer  6716  swoord1  6717  swoord2  6718  fimax2gtrilemstep  7071  iunfidisj  7124  ssfii  7152  suplub2ti  7179  prarloclem3  7695  fzosubel3  10414  seq3split  10722  seqsplitg  10723  seq3caopr  10729  seqcaoprg  10730  zsumdc  11910  fsumiun  12003  divalglemex  12448  pcgcd1  12866  strle1g  13154  prdssgrpd  13463  mnd32g  13475  mnd12g  13476  mnd4g  13477  ismndd  13485  mndinvmod  13493  prdsmndd  13496  imasmnd  13501  grpassd  13560  grpasscan2  13612  grpidrcan  13613  grpidlcan  13614  grpinvinv  13615  grplmulf1o  13622  grpinvssd  13625  grpinvadd  13626  grpsubrcan  13629  grpsubadd  13636  grpaddsubass  13638  grppncan  13639  grpsubsub4  13641  grppnpcan2  13642  grpnpncan  13643  grpnpncan0  13644  grpnnncan2  13645  dfgrp3mlem  13646  dfgrp3m  13647  grplactcnv  13650  imasgrp  13663  mhmmnd  13668  mulgaddcomlem  13697  mulgaddcom  13698  mulgnn0dir  13704  mulgdirlem  13705  mulgneg2  13708  mulgnnass  13709  mulgnn0ass  13710  mulgass  13711  mulgmodid  13713  nsgconj  13758  isnsg3  13759  nmzsubg  13762  ssnmz  13763  eqger  13776  eqgcpbl  13780  conjghm  13828  conjnmz  13831  conjnmzb  13832  abl32  13859  abladdsub4  13866  abladdsub  13867  ablpncan2  13868  ablsubsub  13870  rngass  13917  rnglz  13923  rngrz  13924  rngmneg1  13925  rngmneg2  13926  rngsubdi  13929  rngsubdir  13930  imasrng  13934  srgass  13949  srgmulgass  13967  srgpcomp  13968  srgpcompp  13969  srgpcomppsc  13970  ringass  13994  ringadd2  14005  ringo2times  14006  ringcom  14009  ringlz  14021  ringrz  14022  ringnegl  14029  ringnegr  14030  ringmneg1  14031  ringmneg2  14032  ringsubdi  14034  ringsubdir  14035  mulgass2  14036  imasring  14042  opprrng  14055  opprring  14057  mulgass3  14063  dvdsrtr  14080  dvdsrmul1  14081  unitgrp  14095  dvrass  14118  dvrcan1  14119  dvrcan3  14120  dvrdir  14122  rdivmuldivd  14123  rhmunitinv  14157  lringuplu  14175  subrginv  14216  unitrrg  14246  aprcotr  14264  islmod  14270  lmod0vs  14300  lmodvs0  14301  lmodvsmmulgdi  14302  lmodfopne  14305  lmodvneg1  14309  lmodvsneg  14310  lmodcom  14312  lmodsubvs  14322  lmodsubdi  14323  lmodsubdir  14324  islss3  14358  lss1d  14362  sralmod  14429  rnglidlmsgrp  14476  2idlcpblrng  14502  mulgrhm  14588  psmetsym  15018  psmettri  15019  psmetge0  15020  psmetres2  15022  xmetge0  15054  xmetsym  15057  xmettri  15061  metrtri  15066  xmetres2  15068  bldisj  15090  xblss2ps  15093  xblss2  15094  xmeter  15125  xmetxp  15196  dvdsppwf1o  15678  perfect1  15687  perfectlem1  15688  perfectlem2  15689  3dom  16411