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  6171  caovcand  6174  caovordid  6178  caovordd  6180  caovdid  6187  caovdird  6190  swoer  6716  swoord1  6717  swoord2  6718  fimax2gtrilemstep  7070  iunfidisj  7121  ssfii  7149  suplub2ti  7176  prarloclem3  7692  fzosubel3  10410  seq3split  10718  seqsplitg  10719  seq3caopr  10725  seqcaoprg  10726  zsumdc  11903  fsumiun  11996  divalglemex  12441  pcgcd1  12859  strle1g  13147  prdssgrpd  13456  mnd32g  13468  mnd12g  13469  mnd4g  13470  ismndd  13478  mndinvmod  13486  prdsmndd  13489  imasmnd  13494  grpassd  13553  grpasscan2  13605  grpidrcan  13606  grpidlcan  13607  grpinvinv  13608  grplmulf1o  13615  grpinvssd  13618  grpinvadd  13619  grpsubrcan  13622  grpsubadd  13629  grpaddsubass  13631  grppncan  13632  grpsubsub4  13634  grppnpcan2  13635  grpnpncan  13636  grpnpncan0  13637  grpnnncan2  13638  dfgrp3mlem  13639  dfgrp3m  13640  grplactcnv  13643  imasgrp  13656  mhmmnd  13661  mulgaddcomlem  13690  mulgaddcom  13691  mulgnn0dir  13697  mulgdirlem  13698  mulgneg2  13701  mulgnnass  13702  mulgnn0ass  13703  mulgass  13704  mulgmodid  13706  nsgconj  13751  isnsg3  13752  nmzsubg  13755  ssnmz  13756  eqger  13769  eqgcpbl  13773  conjghm  13821  conjnmz  13824  conjnmzb  13825  abl32  13852  abladdsub4  13859  abladdsub  13860  ablpncan2  13861  ablsubsub  13863  rngass  13910  rnglz  13916  rngrz  13917  rngmneg1  13918  rngmneg2  13919  rngsubdi  13922  rngsubdir  13923  imasrng  13927  srgass  13942  srgmulgass  13960  srgpcomp  13961  srgpcompp  13962  srgpcomppsc  13963  ringass  13987  ringadd2  13998  ringo2times  13999  ringcom  14002  ringlz  14014  ringrz  14015  ringnegl  14022  ringnegr  14023  ringmneg1  14024  ringmneg2  14025  ringsubdi  14027  ringsubdir  14028  mulgass2  14029  imasring  14035  opprrng  14048  opprring  14050  mulgass3  14056  dvdsrtr  14073  dvdsrmul1  14074  unitgrp  14088  dvrass  14111  dvrcan1  14112  dvrcan3  14113  dvrdir  14115  rdivmuldivd  14116  rhmunitinv  14150  lringuplu  14168  subrginv  14209  unitrrg  14239  aprcotr  14257  islmod  14263  lmod0vs  14293  lmodvs0  14294  lmodvsmmulgdi  14295  lmodfopne  14298  lmodvneg1  14302  lmodvsneg  14303  lmodcom  14305  lmodsubvs  14315  lmodsubdi  14316  lmodsubdir  14317  islss3  14351  lss1d  14355  sralmod  14422  rnglidlmsgrp  14469  2idlcpblrng  14495  mulgrhm  14581  psmetsym  15011  psmettri  15012  psmetge0  15013  psmetres2  15015  xmetge0  15047  xmetsym  15050  xmettri  15054  metrtri  15059  xmetres2  15061  bldisj  15083  xblss2ps  15086  xblss2  15087  xmeter  15118  xmetxp  15189  dvdsppwf1o  15671  perfect1  15680  perfectlem1  15681  perfectlem2  15682  3dom  16381