Theorem biantru 300

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 298	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.71  387  mpbiran2  926  isset  2695  rexcom4b  2714  eueq  2859  ssrabeq  3188  a9evsep  4058  pwunim  4216  elvv  4609  elvvv  4610  resopab  4871  funfn  5161  dffn2  5282  dffn3  5291  dffn4  5359  fsn  5600  ixp0x  6628  ac6sfi  6800  fimax2gtri  6803  xrmaxiflemcom  11050  trirec0xor  13413