Theorem 3imp3i2an 1346

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

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  focofo  6788  ordunel  7805  naddel1  8654  distrlem5pr  10987  divmul  11847  modmulnn  13858  modaddid  13879  moddi  13911  repswpfx  14757  shftval2  15048  pcgcd  16856  gsumccat  18775  qussub  19130  gsumdixp  20235  lspun  20900  evlslem4  21990  ordtcld3  23093  sleadd1im  27901  fusgrfisstep  29263  cplgr3v  29369  upgr2pthnlp  29669  frgrreg  30330  eliuniin  45100  eliuniin2  45121  disjinfi  45193