Theorem biantru 528

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

Syntax hints:   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  biantrur  529  pm4.71  556  eu6lem  2565  eu6  2566  issetlem  2811  rextru  3075  rexcom4b  3502  eueq  3703  ssrabeq  4081  nsspssun  4256  disjpss  4459  reusngf  4675  reuprg0  4705  reuprg  4706  pr1eqbg  4856  disjprgw  5142  disjprg  5143  ax6vsep  5302  pwun  5571  dfid3  5576  elvv  5749  elvvv  5750  dfres3  5985  resopab  6033  xpcan2  6175  funfn  6577  dffn2  6718  dffn3  6729  dffn4  6810  fsn  7134  sucexb  7794  fparlem1  8100  wfrlem8OLD  8318  ixp0x  8922  ac6sfi  9289  fiint  9326  rankc1  9867  cf0  10248  ccatrcan  14673  prmreclem2  16854  subislly  23205  ovoliunlem1  25251  plyun0  25946  dmscut  27549  tgjustf  27991  ercgrg  28035  0wlk  29636  0trl  29642  0pth  29645  0cycl  29654  nmoolb  30291  hlimreui  30759  nmoplb  31427  nmfnlb  31444  dmdbr5ati  31942  disjunsn  32092  fsumcvg4  33228  ind1a  33315  issibf  33630  bnj1174  34312  derang0  34458  subfacp1lem6  34474  satfdm  34658  bj-denoteslem  36053  bj-rexcom4bv  36065  bj-rexcom4b  36066  bj-tagex  36171  bj-dfid2ALT  36249  bj-restuni  36281  rdgeqoa  36554  ftc1anclem5  36868  disjressuc2  37561  eqvrelcoss3  37791  dfeldisj5  37894  dibord  40333  ifpnot  42523  ifpdfxor  42540  ifpid1g  42547  ifpim1g  42554  ifpimimb  42557  relopabVD  43964  euabsneu  46036  rmotru  47576  reutru  47577