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  6174  caovcand  6177  caovordid  6181  caovordd  6183  caovdid  6190  caovdird  6193  swoer  6721  swoord1  6722  swoord2  6723  fimax2gtrilemstep  7076  iunfidisj  7129  ssfii  7157  suplub2ti  7184  prarloclem3  7700  fzosubel3  10419  seq3split  10727  seqsplitg  10728  seq3caopr  10734  seqcaoprg  10735  zsumdc  11916  fsumiun  12009  divalglemex  12454  pcgcd1  12872  strle1g  13160  prdssgrpd  13469  mnd32g  13481  mnd12g  13482  mnd4g  13483  ismndd  13491  mndinvmod  13499  prdsmndd  13502  imasmnd  13507  grpassd  13566  grpasscan2  13618  grpidrcan  13619  grpidlcan  13620  grpinvinv  13621  grplmulf1o  13628  grpinvssd  13631  grpinvadd  13632  grpsubrcan  13635  grpsubadd  13642  grpaddsubass  13644  grppncan  13645  grpsubsub4  13647  grppnpcan2  13648  grpnpncan  13649  grpnpncan0  13650  grpnnncan2  13651  dfgrp3mlem  13652  dfgrp3m  13653  grplactcnv  13656  imasgrp  13669  mhmmnd  13674  mulgaddcomlem  13703  mulgaddcom  13704  mulgnn0dir  13710  mulgdirlem  13711  mulgneg2  13714  mulgnnass  13715  mulgnn0ass  13716  mulgass  13717  mulgmodid  13719  nsgconj  13764  isnsg3  13765  nmzsubg  13768  ssnmz  13769  eqger  13782  eqgcpbl  13786  conjghm  13834  conjnmz  13837  conjnmzb  13838  abl32  13865  abladdsub4  13872  abladdsub  13873  ablpncan2  13874  ablsubsub  13876  rngass  13923  rnglz  13929  rngrz  13930  rngmneg1  13931  rngmneg2  13932  rngsubdi  13935  rngsubdir  13936  imasrng  13940  srgass  13955  srgmulgass  13973  srgpcomp  13974  srgpcompp  13975  srgpcomppsc  13976  ringass  14000  ringadd2  14011  ringo2times  14012  ringcom  14015  ringlz  14027  ringrz  14028  ringnegl  14035  ringnegr  14036  ringmneg1  14037  ringmneg2  14038  ringsubdi  14040  ringsubdir  14041  mulgass2  14042  imasring  14048  opprrng  14061  opprring  14063  mulgass3  14069  dvdsrtr  14086  dvdsrmul1  14087  unitgrp  14101  dvrass  14124  dvrcan1  14125  dvrcan3  14126  dvrdir  14128  rdivmuldivd  14129  rhmunitinv  14163  lringuplu  14181  subrginv  14222  unitrrg  14252  aprcotr  14270  islmod  14276  lmod0vs  14306  lmodvs0  14307  lmodvsmmulgdi  14308  lmodfopne  14311  lmodvneg1  14315  lmodvsneg  14316  lmodcom  14318  lmodsubvs  14328  lmodsubdi  14329  lmodsubdir  14330  islss3  14364  lss1d  14368  sralmod  14435  rnglidlmsgrp  14482  2idlcpblrng  14508  mulgrhm  14594  psmetsym  15024  psmettri  15025  psmetge0  15026  psmetres2  15028  xmetge0  15060  xmetsym  15063  xmettri  15067  metrtri  15072  xmetres2  15074  bldisj  15096  xblss2ps  15099  xblss2  15100  xmeter  15131  xmetxp  15202  dvdsppwf1o  15684  perfect1  15693  perfectlem1  15694  perfectlem2  15695  3dom  16465