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  2654  eu6  2655  isset  3507  rexcom4b  3525  eueq  3699  ssrabeq  4059  nsspssun  4234  disjpss  4410  reusngf  4606  reuprg0  4632  reuprg  4633  pr1eqbg  4781  disjprgw  5054  disjprg  5055  ax6vsep  5200  pwun  5453  dfid3  5457  elvv  5621  elvvv  5622  dfres3  5853  resopab  5897  xpcan2  6029  funfn  6380  dffn2  6511  dffn3  6520  dffn4  6591  fsn  6892  sucexb  7518  fparlem1  7801  fsplitOLD  7807  wfrlem8  7956  ixp0x  8484  ac6sfi  8756  fiint  8789  rankc1  9293  cf0  9667  ccatrcan  14075  prmreclem2  16247  subislly  22083  ovoliunlem1  24097  plyun0  24781  tgjustf  26253  ercgrg  26297  0wlk  27889  0trl  27895  0pth  27898  0cycl  27907  nmoolb  28542  hlimreui  29010  nmoplb  29678  nmfnlb  29695  dmdbr5ati  30193  disjunsn  30338  fsumcvg4  31188  ind1a  31273  issibf  31586  bnj1174  32270  derang0  32411  subfacp1lem6  32427  satfdm  32611  dmscut  33267  bj-denotes  34183  bj-rexcom4bv  34193  bj-rexcom4b  34194  bj-tagex  34294  bj-restuni  34382  rdgeqoa  34645  ftc1anclem5  34965  eqvrelcoss3  35847  dfeldisj5  35948  dibord  38289  ifpnot  39828  ifpdfxor  39846  ifpid1g  39853  ifpim1g  39860  ifpimimb  39863  relopabVD  41228  euabsneu  43256