Theorem syl13anc 1280

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl23anc  1285  syl33anc  1293  caovassd  6249  caovcand  6252  caovordid  6256  caovordd  6258  caovdid  6265  caovdird  6268  swoer  6835  swoord1  6836  swoord2  6837  fimax2gtrilemstep  7205  iunfidisj  7260  ssfii  7308  suplub2ti  7341  prarloclem3  7864  fzosubel3  10616  seq3split  10927  seqsplitg  10928  seq3caopr  10934  seqcaoprg  10935  zsumdc  12153  fsumiun  12246  divalglemex  12691  pcgcd1  13109  strle1g  13462  mnd32g  13742  mnd12g  13743  mnd4g  13744  ismndd  13752  mndinvmod  13760  imasmnd  13762  grpassd  13819  grpasscan2  13871  grpidrcan  13872  grpidlcan  13873  grpinvinv  13874  grplmulf1o  13881  grpinvssd  13884  grpinvadd  13885  grpsubrcan  13888  grpsubadd  13895  grpaddsubass  13897  grppncan  13898  grpsubsub4  13900  grppnpcan2  13901  grpnpncan  13902  grpnpncan0  13903  grpnnncan2  13904  dfgrp3mlem  13905  dfgrp3m  13906  grplactcnv  13909  imasgrp  13916  mhmmnd  13921  mulgaddcomlem  13950  mulgaddcom  13951  mulgnn0dir  13957  mulgdirlem  13958  mulgneg2  13961  mulgnnass  13962  mulgnn0ass  13963  mulgass  13964  mulgmodid  13966  nsgconj  14011  isnsg3  14012  nmzsubg  14015  ssnmz  14016  eqger  14029  eqgcpbl  14033  conjghm  14081  conjnmz  14084  conjnmzb  14085  abl32  14112  abladdsub4  14120  abladdsub  14121  ablpncan2  14122  ablsubsub  14124  prdssgrpd  14193  prdsmndd  14196  rngass  14240  rnglz  14246  rngrz  14247  rngmneg1  14248  rngmneg2  14249  rngsubdi  14252  rngsubdir  14253  imasrng  14257  srgass  14277  srgmulgass  14295  srgpcomp  14296  srgpcompp  14297  srgpcomppsc  14298  ringass  14322  ringadd2  14334  ringo2times  14335  ringcom  14338  ringlz  14350  ringrz  14351  ringnegl  14358  ringnegr  14359  ringmneg1  14360  ringmneg2  14361  ringsubdi  14363  ringsubdir  14364  mulgass2  14365  imasring  14371  opprrng  14384  opprring  14386  mulgass3  14393  dvdsrtr  14410  dvdsrmul1  14411  unitgrp  14425  dvrass  14448  dvrcan1  14449  dvrcan3  14450  dvrdir  14452  rdivmuldivd  14453  rhmunitinv  14487  lringuplu  14505  subrginv  14547  unitrrg  14578  aprcotr  14599  islmod  14629  lmod0vs  14660  lmodvs0  14661  lmodvsmmulgdi  14662  lmodfopne  14665  lmodvneg1  14669  lmodvsneg  14670  lmodcom  14672  lmodsubvs  14682  lmodsubdi  14683  lmodsubdir  14684  islss3  14718  lss1d  14722  sralmod  14789  rnglidlmsgrp  14836  2idlcpblrng  14862  mulgrhm  14946  assa2ass  15011  assa2ass2  15012  asclghm  15027  asclmul1  15031  asclmul2  15032  ascldimul  15033  assamulgscmlem2  15044  asclmulg  15046  psmetsym  15432  psmettri  15433  psmetge0  15434  psmetres2  15436  xmetge0  15468  xmetsym  15471  xmettri  15475  metrtri  15480  xmetres2  15482  bldisj  15504  xblss2ps  15507  xblss2  15508  xmeter  15539  xmetxp  15610  dvdsppwf1o  16109  perfect1  16118  perfectlem1  16119  perfectlem2  16120  3dom  17030