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  386  mpbiran2  925  isset  2687  rexcom4b  2706  eueq  2850  ssrabeq  3178  a9evsep  4045  pwunim  4203  elvv  4596  elvvv  4597  resopab  4858  funfn  5148  dffn2  5269  dffn3  5278  dffn4  5346  fsn  5585  ixp0x  6613  ac6sfi  6785  fimax2gtri  6788  xrmaxiflemcom  11011