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 196   ∧ 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 197  df-an 385

This theorem is referenced by:  mpbiran  973  cases  1011  truan  1541  2sb5rf  2479  rexv  3251  reuv  3252  rmov  3253  rabab  3254  euxfr  3425  euind  3426  ddif  3775  nssinpss  3889  nsspssun  3890  vss  4045  difsnpss  4370  sspr  4398  sstp  4399  disjprg  4680  mptv  4784  reusv2lem5  4903  oteqex2  4992  dfid4  5055  intirr  5549  xpcan  5605  fvopab6  6350  fnressn  6465  riotav  6656  mpt2v  6792  sorpss  6984  opabn1stprc  7272  fparlem2  7323  fnsuppres  7367  brtpos0  7404  sup0riota  8412  genpass  9869  nnwos  11793  hashbclem  13274  ccatlcan  13518  clim0  14281  gcd0id  15287  pjfval2  20101  mat1dimbas  20326  pmatcollpw2lem  20630  isbasis3g  20801  opnssneib  20967  ssidcn  21107  qtopcld  21564  mdegleb  23869  vieta1  24112  lgsne0  25105  axpasch  25866  0wlk  27094  0clwlk  27108  shlesb1i  28373  chnlei  28472  pjneli  28710  cvexchlem  29355  dmdbr5ati  29409  elimifd  29488  lmxrge0  30126  cntnevol  30419  bnj110  31054  elpotr  31810  dfbigcup2  32131  bj-cleljustab  32972  bj-rexvwv  32991  bj-rababwv  32992  finxpreclem4  33361  wl-cases2-dnf  33425  cnambfre  33588  triantru3  34143  lub0N  34794  glb0N  34798  cvlsupr3  34949  isdomn3  38099  ifpdfor2  38122  ifpdfor  38126  ifpim1  38130  ifpid2  38132  ifpim2  38133  ifpid2g  38155  ifpid1g  38156  ifpim23g  38157  ifpim1g  38163  ifpimimb  38166  rp-isfinite6  38181  rababg  38196  relnonrel  38210  rp-imass  38382  dffrege115  38589  dfnelbr2  41614