This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj240

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

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

Proof

Step Hyp Ref Expression
1 bnj240.1 Could not format ( ps -> ps' ) : No typesetting found for |- ( ps -> ps' ) with typecode |-
2 bnj240.2 Could not format ( ch -> ch' ) : No typesetting found for |- ( ch -> ch' ) with typecode |-
3 1 3ad2ant1 Could not format ( ( ps /\ ch /\ ph ) -> ps' ) : No typesetting found for |- ( ( ps /\ ch /\ ph ) -> ps' ) with typecode |-
4 2 3ad2ant2 Could not format ( ( ps /\ ch /\ ph ) -> ch' ) : No typesetting found for |- ( ( ps /\ ch /\ ph ) -> ch' ) with typecode |-
5 3 4 jca Could not format ( ( ps /\ ch /\ ph ) -> ( ps' /\ ch' ) ) : No typesetting found for |- ( ( ps /\ ch /\ ph ) -> ( ps' /\ ch' ) ) with typecode |-
6 5 3comr Could not format ( ( ph /\ ps /\ ch ) -> ( ps' /\ ch' ) ) : No typesetting found for |- ( ( ph /\ ps /\ ch ) -> ( ps' /\ ch' ) ) with typecode |-