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  4109  pwunim  4269  elvv  4671  elvvv  4672  resopab  4933  funfn  5226  dffn2  5347  dffn3  5356  dffn4  5424  fsn  5665  ixp0x  6700  ac6sfi  6872  fimax2gtri  6875  xrmaxiflemcom  11199  trirec0xor  13999