Theorem 3imp3i2an 1355

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  focofo  6776  ordunel  7792  naddel1  8642  distrlem5pr  10971  divmul  11834  modmulnn  13885  modaddid  13906  moddi  13938  repswpfx  14784  shftval2  15074  pcgcd  16886  gsumccat  18847  qussub  19204  gsumdixp  20335  lspun  21023  evlslem4  22098  ordtcld3  23228  leadds1im  28046  fusgrfisstep  29465  cplgr3v  29571  upgr2pthnlp  29867  frgrreg  30531  eliuniin  45615  eliuniin2  45636  disjinfi  45708