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  944  isset  2783  rexcom4b  2802  eueq  2951  ssrabeq  3288  a9evsep  4182  pwunim  4351  elvv  4755  elvvv  4756  resopab  5022  funfn  5320  dffn2  5447  dffn3  5456  dffn4  5526  fsn  5775  ixp0x  6836  ac6sfi  7021  fimax2gtri  7024  nninfwlporlemd  7300  ccatrcan  11210  xrmaxiflemcom  11675  plyun0  15323  trirec0xor  16186