Metamath Proof Explorer
Description: A chained inference from transitive law for logical equivalence.
(Contributed by NM, 2Sep1995)


Ref 
Expression 

Hypotheses 
3bitr4i.1 
⊢ ( 𝜑 ↔ 𝜓 ) 


3bitr4i.2 
⊢ ( 𝜒 ↔ 𝜑 ) 


3bitr4i.3 
⊢ ( 𝜃 ↔ 𝜓 ) 

Assertion 
3bitr4ri 
⊢ ( 𝜃 ↔ 𝜒 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3bitr4i.1 
⊢ ( 𝜑 ↔ 𝜓 ) 
2 

3bitr4i.2 
⊢ ( 𝜒 ↔ 𝜑 ) 
3 

3bitr4i.3 
⊢ ( 𝜃 ↔ 𝜓 ) 
4 
1 3

bitr4i 
⊢ ( 𝜑 ↔ 𝜃 ) 
5 
2 4

bitr2i 
⊢ ( 𝜃 ↔ 𝜒 ) 