Theorem biantru 300

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

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.71  387  mpbiran2  936  isset  2736  rexcom4b  2755  eueq  2901  ssrabeq  3234  a9evsep  4111  pwunim  4271  elvv  4673  elvvv  4674  resopab  4935  funfn  5228  dffn2  5349  dffn3  5358  dffn4  5426  fsn  5668  ixp0x  6704  ac6sfi  6876  fimax2gtri  6879  nninfwlporlemd  7148  xrmaxiflemcom  11212  trirec0xor  14077