Theorem bnj252 30769

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

Assertion

Ref	Expression
bnj252	|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph /\ ( ps /\ ch /\ th ) ) )

Proof of Theorem bnj252

Step	Hyp	Ref	Expression
1		bnj250 30767	. 2 |- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph /\ ( ( ps /\ ch ) /\ th ) ) )
2		df-3an 1039	. . 3 |- ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
3	2	anbi2i 730	. 2 |- ( ( ph /\ ( ps /\ ch /\ th ) ) <-> ( ph /\ ( ( ps /\ ch ) /\ th ) ) )
4	1, 3	bitr4i 267	1 |- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph /\ ( ps /\ ch /\ th ) ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   /\ w-bnj17 30752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039  df-bnj17 30753

This theorem is referenced by:  bnj290  30776  bnj563  30813  bnj919  30837  bnj976  30848  bnj543  30963  bnj570  30975  bnj594  30982  bnj916  31003  bnj917  31004  bnj964  31013  bnj983  31021  bnj984  31022  bnj998  31026  bnj999  31027  bnj1021  31034  bnj1083  31046  bnj1450  31118