Theorem 3imp3i2an 1364

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2022.)

Hypotheses

Ref	Expression
3imp3i2an.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3imp3i2an.2	⊢ ((𝜑 ∧ 𝜒) → 𝜏)
3imp3i2an.3	⊢ ((𝜃 ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
3imp3i2an	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂)

Proof of Theorem 3imp3i2an

Step	Hyp	Ref	Expression
1		3imp3i2an.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2		3imp3i2an.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜏)
3	2	3adant2 1149	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)
4		3imp3i2an.3	. 2 ⊢ ((𝜃 ∧ 𝜏) → 𝜂)
5	1, 3, 4	syl2anc 596	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  focofo  6839  ordunel  7872  naddel1  8735  distrlem5pr  11151  divmul  12017  modmulnn  14069  modaddid  14090  moddi  14122  repswpfx  14978  shftval2  15271  pcgcd  17100  gsumccat  19087  qussub  19456  gsumdixp  20599  lspun  21313  evlslem4  22440  ordtcld3  23572  leadds1im  28430  fusgrfisstep  29967  cplgr3v  30073  upgr2pthnlp  30375  frgrreg  31052  eliuniin  46387  eliuniin2  46408  disjinfi  46480