Theorem biantrur 526

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

Syntax hints:   ↔ wb 195   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  mpbiran  955  cases  1004  truan  1492  2sb5rf  2439  rexv  3193  reuv  3194  rmov  3195  rabab  3196  euxfr  3359  euind  3360  ddif  3704  nssinpss  3818  nsspssun  3819  vss  3964  difsnpss  4279  sspr  4302  sstp  4303  disjprg  4573  mptv  4674  reusv2lem5  4794  oteqex2  4882  dfid4  4945  intirr  5420  xpcan  5475  fvopab6  6203  fnressn  6308  riotav  6494  mpt2v  6626  sorpss  6818  fparlem2  7143  fnsuppres  7187  brtpos0  7224  sup0riota  8232  genpass  9688  nnwos  11590  hashbclem  13048  ccatlcan  13273  clim0  14034  gcd0id  15027  pjfval2  19820  mat1dimbas  20045  pmatcollpw2lem  20349  isbasis3g  20512  opnssneib  20677  ssidcn  20817  qtopcld  21274  mdegleb  23573  vieta1  23816  lgsne0  24805  axpasch  25567  0wlk  25869  0trl  25870  shlesb1i  27423  chnlei  27522  pjneli  27760  cvexchlem  28405  dmdbr5ati  28459  elimifd  28540  lmxrge0  29120  cntnevol  29412  bnj110  29976  elpotr  30724  nofulllem1  30895  dfbigcup2  30970  bj-rexvwv  31854  bj-rababwv  31855  bj-sspwpwab  32033  finxpreclem4  32201  wl-cases2-dnf  32268  cnambfre  32422  lub0N  33288  glb0N  33292  cvlsupr3  33443  isdomn3  36595  ifpdfor2  36618  ifpdfor  36622  ifpim1  36626  ifpid2  36628  ifpim2  36629  ifpid2g  36651  ifpid1g  36652  ifpim23g  36653  ifpim1g  36659  ifpimimb  36662  rp-isfinite6  36677  rababg  36692  relnonrel  36706  rp-imass  36879  dffrege115  37086  opabn1stprc  40123  01wlk  41276