Theorem biantrur 492

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

Hypothesis

Ref	Expression
biantrur.1	⊢ φ

Assertion

Ref	Expression
biantrur	⊢ (ψ ↔ (φ ∧ ψ))

Proof of Theorem biantrur

Step	Hyp	Ref	Expression
1		biantrur.1	. 2 ⊢ φ
2		ibar 490	. 2 ⊢ (φ → (ψ ↔ (φ ∧ ψ)))
3	1, 2	ax-mp 8	1 ⊢ (ψ ↔ (φ ∧ ψ))

Syntax hints:   ↔ wb 176   ∧ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  mpbiran  884  rexv  2873  reuv  2874  rmov  2875  rabab  2876  euxfr  3022  euind  3023  ddif  3398  nssinpss  3487  nsspssun  3488  vss  3587  elimif  3691  difsnpss  3851  sspr  3869  sstp  3870  elp6  4263  xpkvexg  4285  dfuni12  4291  addcid1  4405  vfinspsslem1  4550  xpcan  5057  ssrnres  5059  fvopabg  5391  fnressn  5438  rnoprab  5576  mptv  5718  mpt2v  5719  dmtxp  5802  pw1fnf1o  5855