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  6175  caovcand  6178  caovordid  6182  caovordd  6184  caovdid  6191  caovdird  6194  swoer  6723  swoord1  6724  swoord2  6725  fimax2gtrilemstep  7081  iunfidisj  7134  ssfii  7162  suplub2ti  7189  prarloclem3  7705  fzosubel3  10429  seq3split  10738  seqsplitg  10739  seq3caopr  10745  seqcaoprg  10746  zsumdc  11932  fsumiun  12025  divalglemex  12470  pcgcd1  12888  strle1g  13176  prdssgrpd  13485  mnd32g  13497  mnd12g  13498  mnd4g  13499  ismndd  13507  mndinvmod  13515  prdsmndd  13518  imasmnd  13523  grpassd  13582  grpasscan2  13634  grpidrcan  13635  grpidlcan  13636  grpinvinv  13637  grplmulf1o  13644  grpinvssd  13647  grpinvadd  13648  grpsubrcan  13651  grpsubadd  13658  grpaddsubass  13660  grppncan  13661  grpsubsub4  13663  grppnpcan2  13664  grpnpncan  13665  grpnpncan0  13666  grpnnncan2  13667  dfgrp3mlem  13668  dfgrp3m  13669  grplactcnv  13672  imasgrp  13685  mhmmnd  13690  mulgaddcomlem  13719  mulgaddcom  13720  mulgnn0dir  13726  mulgdirlem  13727  mulgneg2  13730  mulgnnass  13731  mulgnn0ass  13732  mulgass  13733  mulgmodid  13735  nsgconj  13780  isnsg3  13781  nmzsubg  13784  ssnmz  13785  eqger  13798  eqgcpbl  13802  conjghm  13850  conjnmz  13853  conjnmzb  13854  abl32  13881  abladdsub4  13888  abladdsub  13889  ablpncan2  13890  ablsubsub  13892  rngass  13939  rnglz  13945  rngrz  13946  rngmneg1  13947  rngmneg2  13948  rngsubdi  13951  rngsubdir  13952  imasrng  13956  srgass  13971  srgmulgass  13989  srgpcomp  13990  srgpcompp  13991  srgpcomppsc  13992  ringass  14016  ringadd2  14027  ringo2times  14028  ringcom  14031  ringlz  14043  ringrz  14044  ringnegl  14051  ringnegr  14052  ringmneg1  14053  ringmneg2  14054  ringsubdi  14056  ringsubdir  14057  mulgass2  14058  imasring  14064  opprrng  14077  opprring  14079  mulgass3  14085  dvdsrtr  14102  dvdsrmul1  14103  unitgrp  14117  dvrass  14140  dvrcan1  14141  dvrcan3  14142  dvrdir  14144  rdivmuldivd  14145  rhmunitinv  14179  lringuplu  14197  subrginv  14238  unitrrg  14268  aprcotr  14286  islmod  14292  lmod0vs  14322  lmodvs0  14323  lmodvsmmulgdi  14324  lmodfopne  14327  lmodvneg1  14331  lmodvsneg  14332  lmodcom  14334  lmodsubvs  14344  lmodsubdi  14345  lmodsubdir  14346  islss3  14380  lss1d  14384  sralmod  14451  rnglidlmsgrp  14498  2idlcpblrng  14524  mulgrhm  14610  psmetsym  15040  psmettri  15041  psmetge0  15042  psmetres2  15044  xmetge0  15076  xmetsym  15079  xmettri  15083  metrtri  15088  xmetres2  15090  bldisj  15112  xblss2ps  15115  xblss2  15116  xmeter  15147  xmetxp  15218  dvdsppwf1o  15700  perfect1  15709  perfectlem1  15710  perfectlem2  15711  3dom  16497