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  931  isset  2732  rexcom4b  2751  eueq  2897  ssrabeq  3229  a9evsep  4104  pwunim  4264  elvv  4666  elvvv  4667  resopab  4928  funfn  5218  dffn2  5339  dffn3  5348  dffn4  5416  fsn  5657  ixp0x  6692  ac6sfi  6864  fimax2gtri  6867  xrmaxiflemcom  11190  trirec0xor  13924