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


Ref 
Expression 

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


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


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

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

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

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

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

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

sylbird 
⊢ ( 𝜑 → ( 𝜃 → 𝜏 ) ) 