Theorem biantru 525

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

Syntax hints:   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  pm4.71  660  mpbiran2  956  isset  3180  rexcom4b  3200  eueq  3345  ssrabeq  3651  nsspssun  3819  disjpss  3980  disjprg  4578  ax6vsep  4713  pwun  4946  dfid3  4954  elvv  5100  elvvv  5101  resopab  5366  xpcan2  5490  funfn  5833  dffn2  5960  dffn3  5967  dffn4  6034  fsn  6308  sucexb  6901  fparlem1  7164  fsplit  7169  wfrlem8  7309  ixp0x  7822  ac6sfi  8089  fiint  8122  rankc1  8616  cf0  8956  ccatrcan  13325  prmreclem2  15459  subislly  21094  ovoliunlem1  23077  plyun0  23757  ercgrg  25212  0wlk  26075  0trl  26076  0pth  26100  nmoolb  27010  hlimreui  27480  nmoplb  28150  nmfnlb  28167  dmdbr5ati  28665  rabtru  28723  disjunsn  28789  fsumcvg4  29324  ind1a  29410  issibf  29722  bnj1174  30325  derang0  30405  subfacp1lem6  30421  dfres3  30902  bj-denotes  32052  bj-rexcom4bv  32065  bj-rexcom4b  32066  bj-tagex  32168  bj-restuni  32231  rdgeqoa  32394  ftc1anclem5  32659  dibord  35466  ifpnot  36833  ifpdfxor  36851  ifpid1g  36858  ifpim1g  36865  ifpimimb  36868  relopabVD  38159  funressnfv  39857  pr1eqbg  40313  01wlk  41284  0Trl  41290  0pth-av  41293  0clWlk  41298