Theorem biantru 531

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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  biantrur  532  pm4.71  559  eu6lem  2571  eu6  2572  elisset  2818  isset  3450  rexcom4b  3466  eueq  3648  ssrabeq  4023  nsspssun  4197  disjpss  4400  reusngf  4612  reuprg0  4642  reuprg  4643  pr1eqbg  4793  disjprgw  5076  disjprg  5077  ax6vsep  5236  pwun  5498  dfid3  5503  elvv  5672  elvvv  5673  dfres3  5908  resopab  5954  xpcan2  6095  funfn  6493  dffn2  6632  dffn3  6643  dffn4  6724  fsn  7039  sucexb  7686  fparlem1  7984  wfrlem8OLD  8178  ixp0x  8745  ac6sfi  9106  fiint  9139  rankc1  9676  cf0  10057  ccatrcan  14481  prmreclem2  16667  subislly  22681  ovoliunlem1  24715  plyun0  25407  tgjustf  26883  ercgrg  26927  0wlk  28529  0trl  28535  0pth  28538  0cycl  28547  nmoolb  29182  hlimreui  29650  nmoplb  30318  nmfnlb  30335  dmdbr5ati  30833  disjunsn  30982  fsumcvg4  31949  ind1a  32036  issibf  32349  bnj1174  33032  derang0  33180  subfacp1lem6  33196  satfdm  33380  dmscut  34054  bj-denoteslem  35103  bj-rexcom4bv  35115  bj-rexcom4b  35116  bj-tagex  35225  bj-dfid2ALT  35284  bj-restuni  35316  rdgeqoa  35589  ftc1anclem5  35902  disjressuc2  36602  eqvrelcoss3  36832  dfeldisj5  36935  dibord  39373  ifpnot  41290  ifpdfxor  41307  ifpid1g  41314  ifpim1g  41321  ifpimimb  41324  relopabVD  42734  euabsneu  44766  rextru  46393  rmotru  46394  reutru  46395