Metamath Proof Explorer
Description: More general version of 3imtr4i . Useful for converting conditional
definitions in a formula. (Contributed by NM, 26Oct1995)


Ref 
Expression 

Hypotheses 
3imtr4d.1 
⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) ) 


3imtr4d.2 
⊢ ( 𝜑 → ( 𝜃 ↔ 𝜓 ) ) 


3imtr4d.3 
⊢ ( 𝜑 → ( 𝜏 ↔ 𝜒 ) ) 

Assertion 
3imtr4d 
⊢ ( 𝜑 → ( 𝜃 → 𝜏 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3imtr4d.1 
⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) ) 
2 

3imtr4d.2 
⊢ ( 𝜑 → ( 𝜃 ↔ 𝜓 ) ) 
3 

3imtr4d.3 
⊢ ( 𝜑 → ( 𝜏 ↔ 𝜒 ) ) 
4 
1 3

sylibrd 
⊢ ( 𝜑 → ( 𝜓 → 𝜏 ) ) 
5 
2 4

sylbid 
⊢ ( 𝜑 → ( 𝜃 → 𝜏 ) ) 