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

This theorem is referenced by:  biantrur  530  pm4.71  557  eu6lem  2574  eu6  2575  issettru  2815  issetlem  2817  rextru  3069  rexcom4b  3474  eueq  3668  ssrabeq  4038  nsspssun  4222  disjpss  4415  reusngf  4633  reuprg0  4661  reuprg  4662  pr1eqbg  4815  disjprg  5096  ax6vsep  5250  pwun  5525  dfid3  5530  elvv  5707  elvvv  5708  dfres3  5951  resopab  6001  xpcan2  6143  funfn  6530  dffn2  6672  dffn3  6682  dffn4  6760  fsn  7090  sucexb  7759  fparlem1  8064  ixp0x  8876  ac6sfi  9196  fiint  9239  rankc1  9794  cf0  10173  ccatrcan  14654  prmreclem2  16857  subislly  23437  ovoliunlem1  25471  plyun0  26170  dmcuts  27799  rightge0  27829  tgjustf  28557  ercgrg  28601  dfpth2  29814  0wlk  30203  0trl  30209  0pth  30212  0cycl  30221  nmoolb  30859  hlimreui  31327  nmoplb  31995  nmfnlb  32012  dmdbr5ati  32510  disjunsn  32681  ind1a  32949  esplyind  33752  fsumcvg4  34128  issibf  34511  bnj1174  35179  derang0  35385  subfacp1lem6  35401  satfdm  35585  bj-denoteslem  37119  bj-rexcom4bv  37130  bj-rexcom4b  37131  bj-tagex  37235  bj-dfid2ALT  37313  bj-restuni  37350  rdgeqoa  37625  ftc1anclem5  37948  disjressuc2  38662  eqvrelcoss3  38953  dfeldisj5  39064  dibord  41535  eu6w  43034  ifpnot  43826  ifpdfxor  43843  ifpid1g  43850  ifpim1g  43857  ifpimimb  43860  relopabVD  45256  n0abso  45332  euabsneu  47388  rmotru  49162  reutru  49163