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 ⊢ (𝜑 → 𝜂)

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

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 1011

This theorem is referenced by:  syl23anc  1285  syl33anc  1293  caovassd  6243  caovcand  6246  caovordid  6250  caovordd  6252  caovdid  6259  caovdird  6262  swoer  6829  swoord1  6830  swoord2  6831  fimax2gtrilemstep  7199  iunfidisj  7254  ssfii  7302  suplub2ti  7335  prarloclem3  7858  fzosubel3  10597  seq3split  10908  seqsplitg  10909  seq3caopr  10915  seqcaoprg  10916  zsumdc  12134  fsumiun  12227  divalglemex  12672  pcgcd1  13090  strle1g  13443  mnd32g  13723  mnd12g  13724  mnd4g  13725  ismndd  13733  mndinvmod  13741  imasmnd  13743  grpassd  13800  grpasscan2  13852  grpidrcan  13853  grpidlcan  13854  grpinvinv  13855  grplmulf1o  13862  grpinvssd  13865  grpinvadd  13866  grpsubrcan  13869  grpsubadd  13876  grpaddsubass  13878  grppncan  13879  grpsubsub4  13881  grppnpcan2  13882  grpnpncan  13883  grpnpncan0  13884  grpnnncan2  13885  dfgrp3mlem  13886  dfgrp3m  13887  grplactcnv  13890  imasgrp  13897  mhmmnd  13902  mulgaddcomlem  13931  mulgaddcom  13932  mulgnn0dir  13938  mulgdirlem  13939  mulgneg2  13942  mulgnnass  13943  mulgnn0ass  13944  mulgass  13945  mulgmodid  13947  nsgconj  13992  isnsg3  13993  nmzsubg  13996  ssnmz  13997  eqger  14010  eqgcpbl  14014  conjghm  14062  conjnmz  14065  conjnmzb  14066  abl32  14093  abladdsub4  14101  abladdsub  14102  ablpncan2  14103  ablsubsub  14105  prdssgrpd  14174  prdsmndd  14177  rngass  14221  rnglz  14227  rngrz  14228  rngmneg1  14229  rngmneg2  14230  rngsubdi  14233  rngsubdir  14234  imasrng  14238  srgass  14258  srgmulgass  14276  srgpcomp  14277  srgpcompp  14278  srgpcomppsc  14279  ringass  14303  ringadd2  14315  ringo2times  14316  ringcom  14319  ringlz  14331  ringrz  14332  ringnegl  14339  ringnegr  14340  ringmneg1  14341  ringmneg2  14342  ringsubdi  14344  ringsubdir  14345  mulgass2  14346  imasring  14352  opprrng  14365  opprring  14367  mulgass3  14374  dvdsrtr  14391  dvdsrmul1  14392  unitgrp  14406  dvrass  14429  dvrcan1  14430  dvrcan3  14431  dvrdir  14433  rdivmuldivd  14434  rhmunitinv  14468  lringuplu  14486  subrginv  14528  unitrrg  14559  aprcotr  14580  islmod  14610  lmod0vs  14641  lmodvs0  14642  lmodvsmmulgdi  14643  lmodfopne  14646  lmodvneg1  14650  lmodvsneg  14651  lmodcom  14653  lmodsubvs  14663  lmodsubdi  14664  lmodsubdir  14665  islss3  14699  lss1d  14703  sralmod  14770  rnglidlmsgrp  14817  2idlcpblrng  14843  mulgrhm  14927  assa2ass  14992  assa2ass2  14993  asclghm  15008  asclmul1  15012  asclmul2  15013  ascldimul  15014  assamulgscmlem2  15025  asclmulg  15027  psmetsym  15413  psmettri  15414  psmetge0  15415  psmetres2  15417  xmetge0  15449  xmetsym  15452  xmettri  15456  metrtri  15461  xmetres2  15463  bldisj  15485  xblss2ps  15488  xblss2  15489  xmeter  15520  xmetxp  15591  dvdsppwf1o  16086  perfect1  16095  perfectlem1  16096  perfectlem2  16097  3dom  17001