Theorem 3imp3i2an 1352

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 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)
4		3imp3i2an.3	. 2 ⊢ ((𝜃 ∧ 𝜏) → 𝜂)
5	1, 3, 4	syl2anc 590	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094

This theorem is referenced by:  focofo  6752  ordunel  7767  naddel1  8613  distrlem5pr  10941  divmul  11803  modmulnn  13839  modaddid  13860  moddi  13892  repswpfx  14738  shftval2  15028  pcgcd  16840  gsumccat  18800  qussub  19157  gsumdixp  20289  lspun  20977  evlslem4  22052  ordtcld3  23182  leadds1im  27997  fusgrfisstep  29416  cplgr3v  29522  upgr2pthnlp  29818  frgrreg  30482  eliuniin  45546  eliuniin2  45567  disjinfi  45639