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  2864  rexcom4b  2881  eueq  3009  nsspssun  3489  disjpss  3602  elvvk  4208  eqtfinrelk  4487  phiall  4619  dfid3  4769  resopab  5000  xpcan2  5059  funfn  5137  dffn2  5225  dffn3  5230  dffn4  5276  f1orn  5297  fsn  5433  ce0nnul  6178  ce0nulnc  6185  dmsnfn  6328