Theorem biantru 526

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

Syntax hints:   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  pm4.71  662  mpbiran2  954  isset  3207  rexcom4b  3227  rabtru  3361  eueq  3378  ssrabeq  3689  nsspssun  3857  disjpss  4028  pr1eqbg  4390  disjprg  4648  ax6vsep  4785  pwun  5022  dfid3  5025  elvv  5177  elvvv  5178  dfres3  5403  resopab  5446  xpcan2  5571  funfn  5918  dffn2  6047  dffn3  6054  dffn4  6121  fsn  6402  sucexb  7009  fparlem1  7277  fsplit  7282  wfrlem8  7422  ixp0x  7936  ac6sfi  8204  fiint  8237  rankc1  8733  cf0  9073  ccatrcan  13473  prmreclem2  15621  subislly  21284  ovoliunlem1  23270  plyun0  23953  ercgrg  25412  0wlk  26977  0trl  26983  0pth  26986  0cycl  26994  nmoolb  27626  hlimreui  28096  nmoplb  28766  nmfnlb  28783  dmdbr5ati  29281  disjunsn  29407  fsumcvg4  29996  ind1a  30081  issibf  30395  bnj1174  31071  derang0  31151  subfacp1lem6  31167  dmscut  31918  bj-denotes  32858  bj-rexcom4bv  32871  bj-rexcom4b  32872  bj-tagex  32975  bj-restuni  33050  bj-ismooredr2  33065  rdgeqoa  33218  ftc1anclem5  33489  dibord  36448  ifpnot  37814  ifpdfxor  37832  ifpid1g  37839  ifpim1g  37846  ifpimimb  37849  relopabVD  39137  funressnfv  41208