Theorem biantru 286

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
biantru.1	|- ph

Assertion

Ref	Expression
biantru	|- ( ps <-> ( ps /\ ph ) )

Proof of Theorem biantru

Step	Hyp	Ref	Expression
1		biantru.1	. 2 |- ph
2		iba 284	. 2 |- ( ph -> ( ps <-> ( ps /\ ph ) ) )
3	1, 2	ax-mp 7	1 |- ( ps <-> ( ps /\ ph ) )

Syntax hints:   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm4.71  369  mpbiran2  848  isset  2561  rexcom4b  2579  eueq  2712  ssrabeq  3026  nsspssun  3170  disjpss  3278  a9evsep  3879  pwunim  4023  elvv  4402  elvvv  4403  resopab  4652  funfn  4931  dffn2  5047  dffn3  5053  dffn4  5112  fsn  5335  ac6sfi  6352