Theorem syl13anc 1251

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 1179	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl13anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
7	1, 5, 6	syl2anc 411	1 ⊢ (𝜑 → 𝜂)

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

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 982

This theorem is referenced by:  syl23anc  1256  syl33anc  1264  caovassd  6087  caovcand  6090  caovordid  6094  caovordd  6096  caovdid  6103  caovdird  6106  swoer  6629  swoord1  6630  swoord2  6631  fimax2gtrilemstep  6970  iunfidisj  7021  ssfii  7049  suplub2ti  7076  prarloclem3  7583  fzosubel3  10291  seq3split  10599  seqsplitg  10600  seq3caopr  10606  seqcaoprg  10607  zsumdc  11568  fsumiun  11661  divalglemex  12106  pcgcd1  12524  strle1g  12811  prdssgrpd  13119  mnd32g  13131  mnd12g  13132  mnd4g  13133  ismndd  13141  mndinvmod  13149  prdsmndd  13152  imasmnd  13157  grpassd  13216  grpasscan2  13268  grpidrcan  13269  grpidlcan  13270  grpinvinv  13271  grplmulf1o  13278  grpinvssd  13281  grpinvadd  13282  grpsubrcan  13285  grpsubadd  13292  grpaddsubass  13294  grppncan  13295  grpsubsub4  13297  grppnpcan2  13298  grpnpncan  13299  grpnpncan0  13300  grpnnncan2  13301  dfgrp3mlem  13302  dfgrp3m  13303  grplactcnv  13306  imasgrp  13319  mhmmnd  13324  mulgaddcomlem  13353  mulgaddcom  13354  mulgnn0dir  13360  mulgdirlem  13361  mulgneg2  13364  mulgnnass  13365  mulgnn0ass  13366  mulgass  13367  mulgmodid  13369  nsgconj  13414  isnsg3  13415  nmzsubg  13418  ssnmz  13419  eqger  13432  eqgcpbl  13436  conjghm  13484  conjnmz  13487  conjnmzb  13488  abl32  13515  abladdsub4  13522  abladdsub  13523  ablpncan2  13524  ablsubsub  13526  rngass  13573  rnglz  13579  rngrz  13580  rngmneg1  13581  rngmneg2  13582  rngsubdi  13585  rngsubdir  13586  imasrng  13590  srgass  13605  srgmulgass  13623  srgpcomp  13624  srgpcompp  13625  srgpcomppsc  13626  ringass  13650  ringadd2  13661  ringo2times  13662  ringcom  13665  ringlz  13677  ringrz  13678  ringnegl  13685  ringnegr  13686  ringmneg1  13687  ringmneg2  13688  ringsubdi  13690  ringsubdir  13691  mulgass2  13692  imasring  13698  opprrng  13711  opprring  13713  mulgass3  13719  dvdsrtr  13735  dvdsrmul1  13736  unitgrp  13750  dvrass  13773  dvrcan1  13774  dvrcan3  13775  dvrdir  13777  rdivmuldivd  13778  rhmunitinv  13812  lringuplu  13830  subrginv  13871  unitrrg  13901  aprcotr  13919  islmod  13925  lmod0vs  13955  lmodvs0  13956  lmodvsmmulgdi  13957  lmodfopne  13960  lmodvneg1  13964  lmodvsneg  13965  lmodcom  13967  lmodsubvs  13977  lmodsubdi  13978  lmodsubdir  13979  islss3  14013  lss1d  14017  sralmod  14084  rnglidlmsgrp  14131  2idlcpblrng  14157  mulgrhm  14243  psmetsym  14673  psmettri  14674  psmetge0  14675  psmetres2  14677  xmetge0  14709  xmetsym  14712  xmettri  14716  metrtri  14721  xmetres2  14723  bldisj  14745  xblss2ps  14748  xblss2  14749  xmeter  14780  xmetxp  14851  dvdsppwf1o  15333  perfect1  15342  perfectlem1  15343  perfectlem2  15344