Metamath Proof Explorer
Description: A mixed syllogism inference, useful for applying a definition to both
sides of an implication. (Contributed by NM, 3Jan1993)


Ref 
Expression 

Hypotheses 
3imtr4.1 
⊢ ( 𝜑 → 𝜓 ) 


3imtr4.2 
⊢ ( 𝜒 ↔ 𝜑 ) 


3imtr4.3 
⊢ ( 𝜃 ↔ 𝜓 ) 

Assertion 
3imtr4i 
⊢ ( 𝜒 → 𝜃 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3imtr4.1 
⊢ ( 𝜑 → 𝜓 ) 
2 

3imtr4.2 
⊢ ( 𝜒 ↔ 𝜑 ) 
3 

3imtr4.3 
⊢ ( 𝜃 ↔ 𝜓 ) 
4 
2 1

sylbi 
⊢ ( 𝜒 → 𝜓 ) 
5 
4 3

sylibr 
⊢ ( 𝜒 → 𝜃 ) 