Theorem biantrur 492

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

Hypothesis

Ref	Expression
biantrur.1	|- ph

Assertion

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

Proof of Theorem biantrur

Step	Hyp	Ref	Expression
1		biantrur.1	. 2 |- ph
2		ibar 490	. 2 |- (ph -> (ps <-> (ph /\ ps)))
3	1, 2	ax-mp 5	1 |- (ps <-> (ph /\ ps))

Syntax hints:   <-> wb 176   /\ wa 358

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 177  df-an 360

This theorem is referenced by:  mpbiran  884  rexv  2874  reuv  2875  rmov  2876  rabab  2877  euxfr  3023  euind  3024  ddif  3399  nssinpss  3488  nsspssun  3489  vss  3588  elimif  3692  difsnpss  3852  sspr  3870  sstp  3871  elp6  4264  xpkvexg  4286  dfuni12  4292  addcid1  4406  vfinspsslem1  4551  xpcan  5058  ssrnres  5060  fvopabg  5392  fnressn  5439  rnoprab  5577  mptv  5719  mpt2v  5720  dmtxp  5803  pw1fnf1o  5856