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  6807  ordunel  7836  naddel1  8690  distrlem5pr  11105  divmul  11970  modmulnn  14022  modaddid  14043  moddi  14075  repswpfx  14929  shftval2  15221  pcgcd  17049  gsumccat  19030  qussub  19399  gsumdixp  20541  lspun  21255  evlslem4  22378  ordtcld3  23510  leadds1im  28366  fusgrfisstep  29903  cplgr3v  30009  upgr2pthnlp  30311  frgrreg  30988  eliuniin  46083  eliuniin2  46104  disjinfi  46176