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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  biantrur  530  pm4.71  557  eu6lem  2562  eu6  2563  issetlem  2808  rextru  3072  rexcom4b  3499  eueq  3701  ssrabeq  4078  nsspssun  4253  disjpss  4456  reusngf  4672  reuprg0  4702  reuprg  4703  pr1eqbg  4853  disjprgw  5137  disjprg  5138  ax6vsep  5297  pwun  5568  dfid3  5573  elvv  5746  elvvv  5747  dfres3  5984  resopab  6032  xpcan2  6175  funfn  6577  dffn2  6718  dffn3  6729  dffn4  6811  fsn  7138  sucexb  7801  fparlem1  8111  wfrlem8OLD  8330  ixp0x  8936  ac6sfi  9303  fiint  9340  rankc1  9885  cf0  10266  ccatrcan  14693  prmreclem2  16877  subislly  23372  ovoliunlem1  25418  plyun0  26118  dmscut  27731  tgjustf  28264  ercgrg  28308  0wlk  29913  0trl  29919  0pth  29922  0cycl  29931  nmoolb  30568  hlimreui  31036  nmoplb  31704  nmfnlb  31721  dmdbr5ati  32219  disjunsn  32369  fsumcvg4  33487  ind1a  33574  issibf  33889  bnj1174  34570  derang0  34715  subfacp1lem6  34731  satfdm  34915  bj-denoteslem  36284  bj-rexcom4bv  36296  bj-rexcom4b  36297  bj-tagex  36402  bj-dfid2ALT  36480  bj-restuni  36512  rdgeqoa  36785  ftc1anclem5  37105  disjressuc2  37797  eqvrelcoss3  38027  dfeldisj5  38130  dibord  40569  ifpnot  42823  ifpdfxor  42840  ifpid1g  42847  ifpim1g  42854  ifpimimb  42857  relopabVD  44263  euabsneu  46333  rmotru  47798  reutru  47799