Theorem 3imp3i2an 1343

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  focofo  6697  ordunel  7662  distrlem5pr  10767  divmul  11619  modmulnn  13590  moddi  13640  repswpfx  14479  shftval2  14767  pcgcd  16560  gsumccatOLD  18460  gsumccat  18461  qussub  18797  gsumdixp  19829  lspun  20230  evlslem4  21265  scmatrngiso  21666  ordtcld3  22331  fusgrfisstep  27677  cplgr3v  27783  upgr2pthnlp  28079  frgrreg  28737  naddel1  33818  eliuniin  42602  eliuniin2  42622  disjinfi  42684