Theorem biantru 532

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
biantru.1	⊢ 𝜑

Assertion

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

Proof of Theorem biantru

Step	Hyp	Ref	Expression
1		biantru.1	. 2 ⊢ 𝜑
2		iba 530	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  biantrur  533  pm4.71  560  eu6lem  2658  eu6  2659  isset  3506  rexcom4b  3524  eueq  3699  ssrabeq  4059  nsspssun  4234  disjpss  4410  reusngf  4612  reuprg0  4638  reuprg  4639  pr1eqbg  4787  disjprgw  5061  disjprg  5062  ax6vsep  5207  pwun  5458  dfid3  5462  elvv  5626  elvvv  5627  dfres3  5858  resopab  5902  xpcan2  6034  funfn  6385  dffn2  6516  dffn3  6525  dffn4  6596  fsn  6897  sucexb  7524  fparlem1  7807  fsplitOLD  7813  wfrlem8  7962  ixp0x  8490  ac6sfi  8762  fiint  8795  rankc1  9299  cf0  9673  ccatrcan  14081  prmreclem2  16253  subislly  22089  ovoliunlem1  24103  plyun0  24787  tgjustf  26259  ercgrg  26303  0wlk  27895  0trl  27901  0pth  27904  0cycl  27913  nmoolb  28548  hlimreui  29016  nmoplb  29684  nmfnlb  29701  dmdbr5ati  30199  disjunsn  30344  fsumcvg4  31193  ind1a  31278  issibf  31591  bnj1174  32275  derang0  32416  subfacp1lem6  32432  satfdm  32616  dmscut  33272  bj-denoteslem  34188  bj-rexcom4bv  34201  bj-rexcom4b  34202  bj-tagex  34302  bj-restuni  34391  rdgeqoa  34654  ftc1anclem5  34986  eqvrelcoss3  35868  dfeldisj5  35969  dibord  38310  ifpnot  39855  ifpdfxor  39873  ifpid1g  39880  ifpim1g  39887  ifpimimb  39890  relopabVD  41255  euabsneu  43283