Theorem biantru 302

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

Syntax hints:   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.71  389  mpbiran2  950  isset  2822  rexcom4b  2841  eueq  2991  ssrabeq  3330  a9evsep  4237  pwunim  4412  elvv  4817  elvvv  4818  resopab  5087  funfn  5387  dffn2  5515  dffn3  5524  dffn4  5601  fsn  5854  ixp0x  6974  ac6sfi  7168  fimax2gtri  7172  nninfwlporlemd  7476  ccatrcan  11436  xrmaxiflemcom  11959  plyun0  15727  trirec0xor  16955