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 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.71  393  mpbiran2  954  isset  2828  rexcom4b  2847  eueq  2997  ssrabeq  3336  a9evsep  4255  pwunim  4431  elvv  4837  elvvv  4838  resopab  5107  funfn  5407  dffn2  5535  dffn3  5544  dffn4  5621  fsn  5880  ixp0x  7008  ac6sfi  7202  fimax2gtri  7206  nninfwlporlemd  7512  ccatrcan  11491  xrmaxiflemcom  12015  plyun0  15837  trirec0xor  17094