Theorem biantru 533

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  biantrur  534  pm4.71  561  eu6lem  2633  eu6  2634  isset  3453  rexcom4b  3471  eueq  3647  ssrabeq  4010  nsspssun  4184  disjpss  4368  reusngf  4572  reuprg0  4598  reuprg  4599  pr1eqbg  4747  disjprgw  5025  disjprg  5026  ax6vsep  5171  pwun  5423  dfid3  5427  elvv  5590  elvvv  5591  dfres3  5823  resopab  5869  xpcan2  6001  funfn  6354  dffn2  6489  dffn3  6499  dffn4  6571  fsn  6874  sucexb  7504  fparlem1  7790  fsplitOLD  7796  wfrlem8  7945  ixp0x  8473  ac6sfi  8746  fiint  8779  rankc1  9283  cf0  9662  ccatrcan  14072  prmreclem2  16243  subislly  22086  ovoliunlem1  24106  plyun0  24794  tgjustf  26267  ercgrg  26311  0wlk  27901  0trl  27907  0pth  27910  0cycl  27919  nmoolb  28554  hlimreui  29022  nmoplb  29690  nmfnlb  29707  dmdbr5ati  30205  disjunsn  30357  fsumcvg4  31303  ind1a  31388  issibf  31701  bnj1174  32385  derang0  32529  subfacp1lem6  32545  satfdm  32729  dmscut  33385  bj-denoteslem  34309  bj-rexcom4bv  34322  bj-rexcom4b  34323  bj-tagex  34423  bj-restuni  34512  rdgeqoa  34787  ftc1anclem5  35134  eqvrelcoss3  36013  dfeldisj5  36114  dibord  38455  ifpnot  40178  ifpdfxor  40195  ifpid1g  40202  ifpim1g  40209  ifpimimb  40212  relopabVD  41607  euabsneu  43620