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  6192  caovcand  6195  caovordid  6199  caovordd  6201  caovdid  6208  caovdird  6211  swoer  6773  swoord1  6774  swoord2  6775  fimax2gtrilemstep  7133  iunfidisj  7188  ssfii  7216  suplub2ti  7243  prarloclem3  7760  fzosubel3  10485  seq3split  10794  seqsplitg  10795  seq3caopr  10801  seqcaoprg  10802  zsumdc  12006  fsumiun  12099  divalglemex  12544  pcgcd1  12962  strle1g  13250  prdssgrpd  13559  mnd32g  13571  mnd12g  13572  mnd4g  13573  ismndd  13581  mndinvmod  13589  prdsmndd  13592  imasmnd  13597  grpassd  13656  grpasscan2  13708  grpidrcan  13709  grpidlcan  13710  grpinvinv  13711  grplmulf1o  13718  grpinvssd  13721  grpinvadd  13722  grpsubrcan  13725  grpsubadd  13732  grpaddsubass  13734  grppncan  13735  grpsubsub4  13737  grppnpcan2  13738  grpnpncan  13739  grpnpncan0  13740  grpnnncan2  13741  dfgrp3mlem  13742  dfgrp3m  13743  grplactcnv  13746  imasgrp  13759  mhmmnd  13764  mulgaddcomlem  13793  mulgaddcom  13794  mulgnn0dir  13800  mulgdirlem  13801  mulgneg2  13804  mulgnnass  13805  mulgnn0ass  13806  mulgass  13807  mulgmodid  13809  nsgconj  13854  isnsg3  13855  nmzsubg  13858  ssnmz  13859  eqger  13872  eqgcpbl  13876  conjghm  13924  conjnmz  13927  conjnmzb  13928  abl32  13955  abladdsub4  13962  abladdsub  13963  ablpncan2  13964  ablsubsub  13966  rngass  14014  rnglz  14020  rngrz  14021  rngmneg1  14022  rngmneg2  14023  rngsubdi  14026  rngsubdir  14027  imasrng  14031  srgass  14046  srgmulgass  14064  srgpcomp  14065  srgpcompp  14066  srgpcomppsc  14067  ringass  14091  ringadd2  14102  ringo2times  14103  ringcom  14106  ringlz  14118  ringrz  14119  ringnegl  14126  ringnegr  14127  ringmneg1  14128  ringmneg2  14129  ringsubdi  14131  ringsubdir  14132  mulgass2  14133  imasring  14139  opprrng  14152  opprring  14154  mulgass3  14160  dvdsrtr  14177  dvdsrmul1  14178  unitgrp  14192  dvrass  14215  dvrcan1  14216  dvrcan3  14217  dvrdir  14219  rdivmuldivd  14220  rhmunitinv  14254  lringuplu  14272  subrginv  14313  unitrrg  14343  aprcotr  14361  islmod  14367  lmod0vs  14397  lmodvs0  14398  lmodvsmmulgdi  14399  lmodfopne  14402  lmodvneg1  14406  lmodvsneg  14407  lmodcom  14409  lmodsubvs  14419  lmodsubdi  14420  lmodsubdir  14421  islss3  14455  lss1d  14459  sralmod  14526  rnglidlmsgrp  14573  2idlcpblrng  14599  mulgrhm  14685  psmetsym  15120  psmettri  15121  psmetge0  15122  psmetres2  15124  xmetge0  15156  xmetsym  15159  xmettri  15163  metrtri  15168  xmetres2  15170  bldisj  15192  xblss2ps  15195  xblss2  15196  xmeter  15227  xmetxp  15298  dvdsppwf1o  15783  perfect1  15792  perfectlem1  15793  perfectlem2  15794  3dom  16688