Theorem syl13anc 1276

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
sylXanc.4	⊢ (𝜑 → 𝜏)
syl13anc.5	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl13anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl13anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		sylXanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	2, 3, 4	3jca 1204	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl13anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
7	1, 5, 6	syl2anc 411	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

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 1007

This theorem is referenced by:  syl23anc  1281  syl33anc  1289  caovassd  6222  caovcand  6225  caovordid  6229  caovordd  6231  caovdid  6238  caovdird  6241  swoer  6808  swoord1  6809  swoord2  6810  fimax2gtrilemstep  7171  iunfidisj  7226  ssfii  7274  suplub2ti  7305  prarloclem3  7828  fzosubel3  10563  seq3split  10874  seqsplitg  10875  seq3caopr  10881  seqcaoprg  10882  zsumdc  12095  fsumiun  12188  divalglemex  12633  pcgcd1  13051  strle1g  13403  prdssgrpd  13712  mnd32g  13724  mnd12g  13725  mnd4g  13726  ismndd  13734  mndinvmod  13742  prdsmndd  13745  imasmnd  13750  grpassd  13809  grpasscan2  13861  grpidrcan  13862  grpidlcan  13863  grpinvinv  13864  grplmulf1o  13871  grpinvssd  13874  grpinvadd  13875  grpsubrcan  13878  grpsubadd  13885  grpaddsubass  13887  grppncan  13888  grpsubsub4  13890  grppnpcan2  13891  grpnpncan  13892  grpnpncan0  13893  grpnnncan2  13894  dfgrp3mlem  13895  dfgrp3m  13896  grplactcnv  13899  imasgrp  13912  mhmmnd  13917  mulgaddcomlem  13946  mulgaddcom  13947  mulgnn0dir  13953  mulgdirlem  13954  mulgneg2  13957  mulgnnass  13958  mulgnn0ass  13959  mulgass  13960  mulgmodid  13962  nsgconj  14007  isnsg3  14008  nmzsubg  14011  ssnmz  14012  eqger  14025  eqgcpbl  14029  conjghm  14077  conjnmz  14080  conjnmzb  14081  abl32  14108  abladdsub4  14115  abladdsub  14116  ablpncan2  14117  ablsubsub  14119  rngass  14167  rnglz  14173  rngrz  14174  rngmneg1  14175  rngmneg2  14176  rngsubdi  14179  rngsubdir  14180  imasrng  14184  srgass  14199  srgmulgass  14217  srgpcomp  14218  srgpcompp  14219  srgpcomppsc  14220  ringass  14244  ringadd2  14255  ringo2times  14256  ringcom  14259  ringlz  14271  ringrz  14272  ringnegl  14279  ringnegr  14280  ringmneg1  14281  ringmneg2  14282  ringsubdi  14284  ringsubdir  14285  mulgass2  14286  imasring  14292  opprrng  14305  opprring  14307  mulgass3  14314  dvdsrtr  14331  dvdsrmul1  14332  unitgrp  14346  dvrass  14369  dvrcan1  14370  dvrcan3  14371  dvrdir  14373  rdivmuldivd  14374  rhmunitinv  14408  lringuplu  14426  subrginv  14468  unitrrg  14499  aprcotr  14520  islmod  14551  lmod0vs  14581  lmodvs0  14582  lmodvsmmulgdi  14583  lmodfopne  14586  lmodvneg1  14590  lmodvsneg  14591  lmodcom  14593  lmodsubvs  14603  lmodsubdi  14604  lmodsubdir  14605  islss3  14639  lss1d  14643  sralmod  14710  rnglidlmsgrp  14757  2idlcpblrng  14783  mulgrhm  14869  psmetsym  15306  psmettri  15307  psmetge0  15308  psmetres2  15310  xmetge0  15342  xmetsym  15345  xmettri  15349  metrtri  15354  xmetres2  15356  bldisj  15378  xblss2ps  15381  xblss2  15382  xmeter  15413  xmetxp  15484  dvdsppwf1o  15969  perfect1  15978  perfectlem1  15979  perfectlem2  15980  3dom  16874