Metamath Proof Explorer
Description: An elimination deduction. (Contributed by Alan Sare, 17Oct2017)
(Proof shortened by Wolf Lammen, 13Apr2022)


Ref 
Expression 

Hypotheses 
3imp3i2an.1 
⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 ) 


3imp3i2an.2 
⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝜏 ) 


3imp3i2an.3 
⊢ ( ( 𝜃 ∧ 𝜏 ) → 𝜂 ) 

Assertion 
3imp3i2an 
⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜂 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3imp3i2an.1 
⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 ) 
2 

3imp3i2an.2 
⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝜏 ) 
3 

3imp3i2an.3 
⊢ ( ( 𝜃 ∧ 𝜏 ) → 𝜂 ) 
4 
2

3adant2 
⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜏 ) 
5 
1 4 3

syl2anc 
⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜂 ) 