Theorem biantru 534

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  biantrur  535  pm4.71  562  eu6lem  2593  eu6  2594  elisset  2834  isset  3423  rexcom4b  3441  eueq  3623  ssrabeq  3989  nsspssun  4163  disjpss  4358  reusngf  4570  reuprg0  4596  reuprg  4597  pr1eqbg  4745  disjprgw  5028  disjprg  5029  ax6vsep  5174  pwun  5429  dfid3  5433  elvv  5596  elvvv  5597  dfres3  5829  resopab  5875  xpcan2  6007  funfn  6366  dffn2  6501  dffn3  6511  dffn4  6583  fsn  6889  sucexb  7524  fparlem1  7813  fsplitOLD  7819  wfrlem8  7973  ixp0x  8509  ac6sfi  8788  fiint  8821  rankc1  9325  cf0  9704  ccatrcan  14121  prmreclem2  16301  subislly  22174  ovoliunlem1  24195  plyun0  24886  tgjustf  26359  ercgrg  26403  0wlk  27993  0trl  27999  0pth  28002  0cycl  28011  nmoolb  28646  hlimreui  29114  nmoplb  29782  nmfnlb  29799  dmdbr5ati  30297  disjunsn  30448  fsumcvg4  31414  ind1a  31499  issibf  31812  bnj1174  32496  derang0  32640  subfacp1lem6  32656  satfdm  32840  dmscut  33559  bj-denoteslem  34583  bj-rexcom4bv  34596  bj-rexcom4b  34597  bj-tagex  34697  bj-restuni  34785  rdgeqoa  35060  ftc1anclem5  35407  eqvrelcoss3  36286  dfeldisj5  36387  dibord  38728  ifpnot  40544  ifpdfxor  40561  ifpid1g  40568  ifpim1g  40575  ifpimimb  40578  relopabVD  41973  euabsneu  43979