# Metamath Proof Explorer

## Theorem bnj887

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

Ref Expression
Hypotheses bnj887.1 No typesetting found for |- ( ph <-> ph' ) with typecode |-
bnj887.2 No typesetting found for |- ( ps <-> ps' ) with typecode |-
bnj887.3 No typesetting found for |- ( ch <-> ch' ) with typecode |-
bnj887.4 No typesetting found for |- ( th <-> th' ) with typecode |-
Assertion bnj887 Could not format assertion : No typesetting found for |- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph' /\ ps' /\ ch' /\ th' ) ) with typecode |-

### Proof

Step Hyp Ref Expression
1 bnj887.1 Could not format ( ph <-> ph' ) : No typesetting found for |- ( ph <-> ph' ) with typecode |-
2 bnj887.2 Could not format ( ps <-> ps' ) : No typesetting found for |- ( ps <-> ps' ) with typecode |-
3 bnj887.3 Could not format ( ch <-> ch' ) : No typesetting found for |- ( ch <-> ch' ) with typecode |-
4 bnj887.4 Could not format ( th <-> th' ) : No typesetting found for |- ( th <-> th' ) with typecode |-
5 1 2 3 3anbi123i Could not format ( ( ph /\ ps /\ ch ) <-> ( ph' /\ ps' /\ ch' ) ) : No typesetting found for |- ( ( ph /\ ps /\ ch ) <-> ( ph' /\ ps' /\ ch' ) ) with typecode |-
6 5 4 anbi12i Could not format ( ( ( ph /\ ps /\ ch ) /\ th ) <-> ( ( ph' /\ ps' /\ ch' ) /\ th' ) ) : No typesetting found for |- ( ( ( ph /\ ps /\ ch ) /\ th ) <-> ( ( ph' /\ ps' /\ ch' ) /\ th' ) ) with typecode |-
7 df-bnj17 ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\wedge {\theta }\right)↔\left(\left({\phi }\wedge {\psi }\wedge {\chi }\right)\wedge {\theta }\right)$
8 df-bnj17 Could not format ( ( ph' /\ ps' /\ ch' /\ th' ) <-> ( ( ph' /\ ps' /\ ch' ) /\ th' ) ) : No typesetting found for |- ( ( ph' /\ ps' /\ ch' /\ th' ) <-> ( ( ph' /\ ps' /\ ch' ) /\ th' ) ) with typecode |-
9 6 7 8 3bitr4i Could not format ( ( ph /\ ps /\ ch /\ th ) <-> ( ph' /\ ps' /\ ch' /\ th' ) ) : No typesetting found for |- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph' /\ ps' /\ ch' /\ th' ) ) with typecode |-