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  942  isset  2755  rexcom4b  2774  eueq  2920  ssrabeq  3254  a9evsep  4137  pwunim  4298  elvv  4700  elvvv  4701  resopab  4963  funfn  5258  dffn2  5379  dffn3  5388  dffn4  5456  fsn  5701  ixp0x  6740  ac6sfi  6912  fimax2gtri  6915  nninfwlporlemd  7184  xrmaxiflemcom  11271  trirec0xor  15090