Theorem biantru 491

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

Hypothesis

Ref	Expression
biantru.1	⊢ φ

Assertion

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

Proof of Theorem biantru

Step	Hyp	Ref	Expression
1		biantru.1	. 2 ⊢ φ
2		iba 489	. 2 ⊢ (φ → (ψ ↔ (ψ ∧ φ)))
3	1, 2	ax-mp 5	1 ⊢ (ψ ↔ (ψ ∧ φ))

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:  pm4.71  611  mpbiran2  885  isset  2863  rexcom4b  2880  eueq  3008  nsspssun  3488  disjpss  3601  elvvk  4207  eqtfinrelk  4486  phiall  4618  dfid3  4768  resopab  4999  xpcan2  5058  funfn  5136  dffn2  5224  dffn3  5229  dffn4  5275  f1orn  5296  fsn  5432  ce0nnul  6177  ce0nulnc  6184  dmsnfn  6327