Theorem biantrur 303

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)

Hypothesis

Ref	Expression
biantrur.1	⊢ 𝜑

Assertion

Ref	Expression
biantrur	⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))

Proof of Theorem biantrur

Step	Hyp	Ref	Expression
1		biantrur.1	. 2 ⊢ 𝜑
2		ibar 301	. 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-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbiran  948  truan  1414  rexv  2821  reuv  2822  rmov  2823  rabab  2824  euxfrdc  2992  euind  2993  dfdif3  3317  ddifstab  3339  vss  3542  mptv  4186  regexmidlem1  4631  peano5  4696  intirr  5123  fvopab6  5743  riotav  5976  mpov  6110  opabn1stprc  6357  brtpos0  6417  frec0g  6562  inl11  7263  apreim  8782  ccatlcan  11298  clim0  11845  gcd0id  12549  nnwosdc  12609  gsum0g  13478  isbasis3g  14769  opnssneib  14879  ssidcn  14933  bj-d0clsepcl  16520