Metamath Proof Explorer


Theorem 3bitr4ri

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995)

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 ( 𝜃𝜒 )