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  2574  eu6  2575  elisset  2821  isset  3443  rexcom4b  3459  eueq  3646  ssrabeq  4021  nsspssun  4196  disjpss  4399  reusngf  4613  reuprg0  4643  reuprg  4644  pr1eqbg  4792  disjprgw  5073  disjprg  5074  ax6vsep  5230  pwun  5486  dfid3  5491  elvv  5660  elvvv  5661  dfres3  5893  resopab  5939  xpcan2  6077  funfn  6460  dffn2  6598  dffn3  6609  dffn4  6690  fsn  7001  sucexb  7644  fparlem1  7936  fsplitOLD  7942  wfrlem8OLD  8131  ixp0x  8688  ac6sfi  9019  fiint  9052  rankc1  9612  cf0  9991  ccatrcan  14413  prmreclem2  16599  subislly  22613  ovoliunlem1  24647  plyun0  25339  tgjustf  26815  ercgrg  26859  0wlk  28459  0trl  28465  0pth  28468  0cycl  28477  nmoolb  29112  hlimreui  29580  nmoplb  30248  nmfnlb  30265  dmdbr5ati  30763  disjunsn  30912  fsumcvg4  31879  ind1a  31966  issibf  32279  bnj1174  32962  derang0  33110  subfacp1lem6  33126  satfdm  33310  dmscut  33984  bj-denoteslem  35034  bj-rexcom4bv  35046  bj-rexcom4b  35047  bj-tagex  35156  bj-dfid2ALT  35215  bj-restuni  35247  rdgeqoa  35520  ftc1anclem5  35833  eqvrelcoss3  36710  dfeldisj5  36811  dibord  39152  ifpnot  41039  ifpdfxor  41056  ifpid1g  41063  ifpim1g  41070  ifpimimb  41073  relopabVD  42474  euabsneu  44473  rextru  46101  rmotru  46102  reutru  46103