Theorem syl13anc 1273

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

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  6156  caovcand  6159  caovordid  6163  caovordd  6165  caovdid  6172  caovdird  6175  swoer  6698  swoord1  6699  swoord2  6700  fimax2gtrilemstep  7050  iunfidisj  7101  ssfii  7129  suplub2ti  7156  prarloclem3  7672  fzosubel3  10389  seq3split  10697  seqsplitg  10698  seq3caopr  10704  seqcaoprg  10705  zsumdc  11881  fsumiun  11974  divalglemex  12419  pcgcd1  12837  strle1g  13125  prdssgrpd  13434  mnd32g  13446  mnd12g  13447  mnd4g  13448  ismndd  13456  mndinvmod  13464  prdsmndd  13467  imasmnd  13472  grpassd  13531  grpasscan2  13583  grpidrcan  13584  grpidlcan  13585  grpinvinv  13586  grplmulf1o  13593  grpinvssd  13596  grpinvadd  13597  grpsubrcan  13600  grpsubadd  13607  grpaddsubass  13609  grppncan  13610  grpsubsub4  13612  grppnpcan2  13613  grpnpncan  13614  grpnpncan0  13615  grpnnncan2  13616  dfgrp3mlem  13617  dfgrp3m  13618  grplactcnv  13621  imasgrp  13634  mhmmnd  13639  mulgaddcomlem  13668  mulgaddcom  13669  mulgnn0dir  13675  mulgdirlem  13676  mulgneg2  13679  mulgnnass  13680  mulgnn0ass  13681  mulgass  13682  mulgmodid  13684  nsgconj  13729  isnsg3  13730  nmzsubg  13733  ssnmz  13734  eqger  13747  eqgcpbl  13751  conjghm  13799  conjnmz  13802  conjnmzb  13803  abl32  13830  abladdsub4  13837  abladdsub  13838  ablpncan2  13839  ablsubsub  13841  rngass  13888  rnglz  13894  rngrz  13895  rngmneg1  13896  rngmneg2  13897  rngsubdi  13900  rngsubdir  13901  imasrng  13905  srgass  13920  srgmulgass  13938  srgpcomp  13939  srgpcompp  13940  srgpcomppsc  13941  ringass  13965  ringadd2  13976  ringo2times  13977  ringcom  13980  ringlz  13992  ringrz  13993  ringnegl  14000  ringnegr  14001  ringmneg1  14002  ringmneg2  14003  ringsubdi  14005  ringsubdir  14006  mulgass2  14007  imasring  14013  opprrng  14026  opprring  14028  mulgass3  14034  dvdsrtr  14050  dvdsrmul1  14051  unitgrp  14065  dvrass  14088  dvrcan1  14089  dvrcan3  14090  dvrdir  14092  rdivmuldivd  14093  rhmunitinv  14127  lringuplu  14145  subrginv  14186  unitrrg  14216  aprcotr  14234  islmod  14240  lmod0vs  14270  lmodvs0  14271  lmodvsmmulgdi  14272  lmodfopne  14275  lmodvneg1  14279  lmodvsneg  14280  lmodcom  14282  lmodsubvs  14292  lmodsubdi  14293  lmodsubdir  14294  islss3  14328  lss1d  14332  sralmod  14399  rnglidlmsgrp  14446  2idlcpblrng  14472  mulgrhm  14558  psmetsym  14988  psmettri  14989  psmetge0  14990  psmetres2  14992  xmetge0  15024  xmetsym  15027  xmettri  15031  metrtri  15036  xmetres2  15038  bldisj  15060  xblss2ps  15063  xblss2  15064  xmeter  15095  xmetxp  15166  dvdsppwf1o  15648  perfect1  15657  perfectlem1  15658  perfectlem2  15659