Metamath Proof Explorer


Theorem bnj887

Description: /\ -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj887.1 ( 𝜑𝜑′ )
bnj887.2 ( 𝜓𝜓′ )
bnj887.3 ( 𝜒𝜒′ )
bnj887.4 ( 𝜃𝜃′ )
Assertion bnj887 ( ( 𝜑𝜓𝜒𝜃 ) ↔ ( 𝜑′𝜓′𝜒′𝜃′ ) )

Proof

Step Hyp Ref Expression
1 bnj887.1 ( 𝜑𝜑′ )
2 bnj887.2 ( 𝜓𝜓′ )
3 bnj887.3 ( 𝜒𝜒′ )
4 bnj887.4 ( 𝜃𝜃′ )
5 1 2 3 3anbi123i ( ( 𝜑𝜓𝜒 ) ↔ ( 𝜑′𝜓′𝜒′ ) )
6 5 4 anbi12i ( ( ( 𝜑𝜓𝜒 ) ∧ 𝜃 ) ↔ ( ( 𝜑′𝜓′𝜒′ ) ∧ 𝜃′ ) )
7 df-bnj17 ( ( 𝜑𝜓𝜒𝜃 ) ↔ ( ( 𝜑𝜓𝜒 ) ∧ 𝜃 ) )
8 df-bnj17 ( ( 𝜑′𝜓′𝜒′𝜃′ ) ↔ ( ( 𝜑′𝜓′𝜒′ ) ∧ 𝜃′ ) )
9 6 7 8 3bitr4i ( ( 𝜑𝜓𝜒𝜃 ) ↔ ( 𝜑′𝜓′𝜒′𝜃′ ) )