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  6213  caovcand  6216  caovordid  6220  caovordd  6222  caovdid  6229  caovdird  6232  swoer  6794  swoord1  6795  swoord2  6796  fimax2gtrilemstep  7157  iunfidisj  7212  ssfii  7260  suplub2ti  7291  prarloclem3  7811  fzosubel3  10540  seq3split  10849  seqsplitg  10850  seq3caopr  10856  seqcaoprg  10857  zsumdc  12066  fsumiun  12159  divalglemex  12604  pcgcd1  13022  strle1g  13311  prdssgrpd  13620  mnd32g  13632  mnd12g  13633  mnd4g  13634  ismndd  13642  mndinvmod  13650  prdsmndd  13653  imasmnd  13658  grpassd  13717  grpasscan2  13769  grpidrcan  13770  grpidlcan  13771  grpinvinv  13772  grplmulf1o  13779  grpinvssd  13782  grpinvadd  13783  grpsubrcan  13786  grpsubadd  13793  grpaddsubass  13795  grppncan  13796  grpsubsub4  13798  grppnpcan2  13799  grpnpncan  13800  grpnpncan0  13801  grpnnncan2  13802  dfgrp3mlem  13803  dfgrp3m  13804  grplactcnv  13807  imasgrp  13820  mhmmnd  13825  mulgaddcomlem  13854  mulgaddcom  13855  mulgnn0dir  13861  mulgdirlem  13862  mulgneg2  13865  mulgnnass  13866  mulgnn0ass  13867  mulgass  13868  mulgmodid  13870  nsgconj  13915  isnsg3  13916  nmzsubg  13919  ssnmz  13920  eqger  13933  eqgcpbl  13937  conjghm  13985  conjnmz  13988  conjnmzb  13989  abl32  14016  abladdsub4  14023  abladdsub  14024  ablpncan2  14025  ablsubsub  14027  rngass  14075  rnglz  14081  rngrz  14082  rngmneg1  14083  rngmneg2  14084  rngsubdi  14087  rngsubdir  14088  imasrng  14092  srgass  14107  srgmulgass  14125  srgpcomp  14126  srgpcompp  14127  srgpcomppsc  14128  ringass  14152  ringadd2  14163  ringo2times  14164  ringcom  14167  ringlz  14179  ringrz  14180  ringnegl  14187  ringnegr  14188  ringmneg1  14189  ringmneg2  14190  ringsubdi  14192  ringsubdir  14193  mulgass2  14194  imasring  14200  opprrng  14213  opprring  14215  mulgass3  14221  dvdsrtr  14238  dvdsrmul1  14239  unitgrp  14253  dvrass  14276  dvrcan1  14277  dvrcan3  14278  dvrdir  14280  rdivmuldivd  14281  rhmunitinv  14315  lringuplu  14333  subrginv  14374  unitrrg  14405  aprcotr  14423  islmod  14431  lmod0vs  14461  lmodvs0  14462  lmodvsmmulgdi  14463  lmodfopne  14466  lmodvneg1  14470  lmodvsneg  14471  lmodcom  14473  lmodsubvs  14483  lmodsubdi  14484  lmodsubdir  14485  islss3  14519  lss1d  14523  sralmod  14590  rnglidlmsgrp  14637  2idlcpblrng  14663  mulgrhm  14749  psmetsym  15186  psmettri  15187  psmetge0  15188  psmetres2  15190  xmetge0  15222  xmetsym  15225  xmettri  15229  metrtri  15234  xmetres2  15236  bldisj  15258  xblss2ps  15261  xblss2  15262  xmeter  15293  xmetxp  15364  dvdsppwf1o  15849  perfect1  15858  perfectlem1  15859  perfectlem2  15860  3dom  16754