Theorem biantru 529

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  biantrur  530  pm4.71  557  eu6lem  2571  eu6  2572  issettru  2812  issetlem  2814  rextru  3065  rexcom4b  3470  eueq  3664  ssrabeq  4034  nsspssun  4218  disjpss  4411  reusngf  4629  reuprg0  4657  reuprg  4658  pr1eqbg  4811  disjprg  5092  ax6vsep  5246  pwun  5515  dfid3  5520  elvv  5697  elvvv  5698  dfres3  5941  resopab  5991  xpcan2  6133  funfn  6520  dffn2  6662  dffn3  6672  dffn4  6750  fsn  7078  sucexb  7747  fparlem1  8052  ixp0x  8862  ac6sfi  9182  fiint  9225  rankc1  9780  cf0  10159  ccatrcan  14640  prmreclem2  16843  subislly  23423  ovoliunlem1  25457  plyun0  26156  dmscut  27779  rightpos  27809  tgjustf  28494  ercgrg  28538  dfpth2  29751  0wlk  30140  0trl  30146  0pth  30149  0cycl  30158  nmoolb  30795  hlimreui  31263  nmoplb  31931  nmfnlb  31948  dmdbr5ati  32446  disjunsn  32618  ind1a  32887  esplyind  33680  fsumcvg4  34056  issibf  34439  bnj1174  35108  derang0  35312  subfacp1lem6  35328  satfdm  35512  bj-denoteslem  37015  bj-rexcom4bv  37026  bj-rexcom4b  37027  bj-tagex  37131  bj-dfid2ALT  37209  bj-restuni  37241  rdgeqoa  37514  ftc1anclem5  37837  disjressuc2  38535  eqvrelcoss3  38814  dfeldisj5  38919  dibord  41358  eu6w  42861  ifpnot  43653  ifpdfxor  43670  ifpid1g  43677  ifpim1g  43684  ifpimimb  43687  relopabVD  45083  n0abso  45159  euabsneu  47216  rmotru  48990  reutru  48991