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  2568  eu6  2569  issetlem  2814  rextru  3078  rexcom4b  3504  eueq  3704  ssrabeq  4082  nsspssun  4257  disjpss  4460  reusngf  4676  reuprg0  4706  reuprg  4707  pr1eqbg  4857  disjprgw  5143  disjprg  5144  ax6vsep  5303  pwun  5572  dfid3  5577  elvv  5749  elvvv  5750  dfres3  5985  resopab  6033  xpcan2  6174  funfn  6576  dffn2  6717  dffn3  6728  dffn4  6809  fsn  7130  sucexb  7789  fparlem1  8095  wfrlem8OLD  8313  ixp0x  8917  ac6sfi  9284  fiint  9321  rankc1  9862  cf0  10243  ccatrcan  14666  prmreclem2  16847  subislly  22977  ovoliunlem1  25011  plyun0  25703  dmscut  27302  tgjustf  27714  ercgrg  27758  0wlk  29359  0trl  29365  0pth  29368  0cycl  29377  nmoolb  30012  hlimreui  30480  nmoplb  31148  nmfnlb  31165  dmdbr5ati  31663  disjunsn  31813  fsumcvg4  32919  ind1a  33006  issibf  33321  bnj1174  34003  derang0  34149  subfacp1lem6  34165  satfdm  34349  bj-denoteslem  35739  bj-rexcom4bv  35751  bj-rexcom4b  35752  bj-tagex  35857  bj-dfid2ALT  35935  bj-restuni  35967  rdgeqoa  36240  ftc1anclem5  36554  disjressuc2  37247  eqvrelcoss3  37477  dfeldisj5  37580  dibord  40019  ifpnot  42207  ifpdfxor  42224  ifpid1g  42231  ifpim1g  42238  ifpimimb  42241  relopabVD  43648  euabsneu  45725  rmotru  47443  reutru  47444