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  6802  ordunel  7823  naddel1  8676  distrlem5pr  11036  divmul  11899  modmulnn  13950  modaddid  13971  moddi  14003  repswpfx  14856  shftval2  15148  pcgcd  16970  gsumccat  18950  qussub  19319  gsumdixp  20459  lspun  21171  evlslem4  22292  ordtcld3  23424  leadds1im  28252  fusgrfisstep  29789  cplgr3v  29895  upgr2pthnlp  30197  frgrreg  30874  eliuniin  45931  eliuniin2  45952  disjinfi  46024