Metamath Proof Explorer


Theorem bnj240

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

Ref Expression
Hypotheses bnj240.1
|- ( ps -> ps' )
bnj240.2
|- ( ch -> ch' )
Assertion bnj240
|- ( ( ph /\ ps /\ ch ) -> ( ps' /\ ch' ) )

Proof

Step Hyp Ref Expression
1 bnj240.1
 |-  ( ps -> ps' )
2 bnj240.2
 |-  ( ch -> ch' )
3 1 3ad2ant1
 |-  ( ( ps /\ ch /\ ph ) -> ps' )
4 2 3ad2ant2
 |-  ( ( ps /\ ch /\ ph ) -> ch' )
5 3 4 jca
 |-  ( ( ps /\ ch /\ ph ) -> ( ps' /\ ch' ) )
6 5 3comr
 |-  ( ( ph /\ ps /\ ch ) -> ( ps' /\ ch' ) )