Theorem syl13anc 1240

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 1177	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl13anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
7	1, 5, 6	syl2anc 411	1 ⊢ (𝜑 → 𝜂)

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

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 980

This theorem is referenced by:  syl23anc  1245  syl33anc  1253  caovassd  6033  caovcand  6036  caovordid  6040  caovordd  6042  caovdid  6049  caovdird  6052  swoer  6562  swoord1  6563  swoord2  6564  fimax2gtrilemstep  6899  iunfidisj  6944  ssfii  6972  suplub2ti  6999  prarloclem3  7495  fzosubel3  10195  seq3split  10478  seq3caopr  10482  zsumdc  11391  fsumiun  11484  divalglemex  11926  pcgcd1  12326  strle1g  12564  mnd32g  12827  mnd12g  12828  mnd4g  12829  ismndd  12837  mndinvmod  12845  grpasscan2  12933  grpidrcan  12934  grpidlcan  12935  grpinvinv  12936  grplmulf1o  12943  grpinvssd  12946  grpinvadd  12947  grpsubrcan  12950  grpsubadd  12957  grpaddsubass  12959  grppncan  12960  grpsubsub4  12962  grppnpcan2  12963  grpnpncan  12964  grpnpncan0  12965  grpnnncan2  12966  dfgrp3mlem  12967  dfgrp3m  12968  grplactcnv  12971  mhmmnd  12979  mulgaddcomlem  13004  mulgaddcom  13005  mulgnn0dir  13011  mulgdirlem  13012  mulgneg2  13015  mulgnnass  13016  mulgnn0ass  13017  mulgass  13018  mulgmodid  13020  nsgconj  13064  isnsg3  13065  nmzsubg  13068  ssnmz  13069  eqger  13081  eqgcpbl  13085  abl32  13108  abladdsub4  13115  abladdsub  13116  ablpncan2  13117  ablsubsub  13119  srgass  13152  srgmulgass  13170  srgpcomp  13171  srgpcompp  13172  srgpcomppsc  13173  ringass  13197  ringadd2  13208  rngo2times  13209  ringcom  13212  ringlz  13220  ringrz  13221  ringnegl  13226  rngnegr  13227  ringmneg1  13228  ringmneg2  13229  ringsubdi  13231  rngsubdir  13232  mulgass2  13233  opprring  13247  mulgass3  13252  dvdsrtr  13268  dvdsrmul1  13269  unitgrp  13283  dvrass  13306  dvrcan1  13307  dvrcan3  13308  dvrdir  13310  rdivmuldivd  13311  lringuplu  13335  aprcotr  13341  subrginv  13363  psmetsym  13765  psmettri  13766  psmetge0  13767  psmetres2  13769  xmetge0  13801  xmetsym  13804  xmettri  13808  metrtri  13813  xmetres2  13815  bldisj  13837  xblss2ps  13840  xblss2  13841  xmeter  13872  xmetxp  13943