Metamath Proof Explorer
Description: Infer implication from a logical equivalence. Similar to biimpar .
(Contributed by NM, 2Jan2009)


Ref 
Expression 

Hypothesis 
biimp3a.1 
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) ) 

Assertion 
biimp3ar 
⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜃 ) → 𝜒 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

biimp3a.1 
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ↔ 𝜃 ) ) 
2 
1

exbiri 
⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜒 ) ) ) 
3 
2

3imp 
⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜃 ) → 𝜒 ) 