Metamath Proof Explorer
Description: Variant of al2imi with conjunctive antecedent. (Contributed by Andrew
Salmon, 8Jun2011)


Ref 
Expression 

Hypothesis 
alanimi.1 
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) 

Assertion 
alanimi 
⊢ ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) → ∀ 𝑥 𝜒 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

alanimi.1 
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) 
2 
1

ex 
⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) ) 
3 
2

al2imi 
⊢ ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) 
4 
3

imp 
⊢ ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) → ∀ 𝑥 𝜒 ) 