Theorem biantrur 528

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 526	. 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  991  cases  1029  truan  1648  2sb5rf  2586  rexv  3358  reuv  3359  rmov  3360  rabab  3361  euxfr  3531  euind  3532  dfdif3  3861  ddif  3883  nssinpss  3997  nsspssun  3998  vss  4153  difsnpss  4481  sspr  4509  sstp  4510  disjprg  4798  mptv  4901  reusv2lem5  5020  oteqex2  5109  dfid4  5174  intirr  5670  xpcan  5726  fvopab6  6471  fnressn  6586  riotav  6777  mpt2v  6913  sorpss  7105  opabn1stprc  7393  fparlem2  7444  fnsuppres  7489  brtpos0  7526  sup0riota  8534  genpass  10021  nnwos  11946  hashbclem  13426  ccatlcan  13670  clim0  14434  gcd0id  15440  pjfval2  20253  mat1dimbas  20478  pmatcollpw2lem  20782  isbasis3g  20953  opnssneib  21119  ssidcn  21259  qtopcld  21716  mdegleb  24021  vieta1  24264  lgsne0  25257  axpasch  26018  0wlk  27266  0clwlk  27280  shlesb1i  28552  chnlei  28651  pjneli  28889  cvexchlem  29534  dmdbr5ati  29588  elimifd  29667  lmxrge0  30305  cntnevol  30598  bnj110  31233  elpotr  31989  dfbigcup2  32310  bj-cleljustab  33151  bj-rexvwv  33170  bj-rababwv  33171  finxpreclem4  33540  wl-cases2-dnf  33606  cnambfre  33769  triantru3  34324  lub0N  34977  glb0N  34981  cvlsupr3  35132  isdomn3  38282  ifpdfor2  38305  ifpdfor  38309  ifpim1  38313  ifpid2  38315  ifpim2  38316  ifpid2g  38338  ifpid1g  38339  ifpim23g  38340  ifpim1g  38346  ifpimimb  38349  rp-isfinite6  38364  rababg  38379  relnonrel  38393  rp-imass  38565  dffrege115  38772  dfnelbr2  41797