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  2820  rexcom4b  2839  eueq  2988  ssrabeq  3326  a9evsep  4232  pwunim  4407  elvv  4812  elvvv  4813  resopab  5082  funfn  5382  dffn2  5510  dffn3  5519  dffn4  5596  fsn  5849  ixp0x  6961  ac6sfi  7155  fimax2gtri  7159  nninfwlporlemd  7463  ccatrcan  11411  xrmaxiflemcom  11934  plyun0  15601  trirec0xor  16829