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  2573  eu6  2574  issettru  2814  issetlem  2816  rextru  3067  rexcom4b  3472  eueq  3666  ssrabeq  4036  nsspssun  4220  disjpss  4413  reusngf  4631  reuprg0  4659  reuprg  4660  pr1eqbg  4813  disjprg  5094  ax6vsep  5248  pwun  5517  dfid3  5522  elvv  5699  elvvv  5700  dfres3  5943  resopab  5993  xpcan2  6135  funfn  6522  dffn2  6664  dffn3  6674  dffn4  6752  fsn  7080  sucexb  7749  fparlem1  8054  ixp0x  8864  ac6sfi  9184  fiint  9227  rankc1  9782  cf0  10161  ccatrcan  14642  prmreclem2  16845  subislly  23425  ovoliunlem1  25459  plyun0  26158  dmcuts  27787  rightge0  27817  tgjustf  28545  ercgrg  28589  dfpth2  29802  0wlk  30191  0trl  30197  0pth  30200  0cycl  30209  nmoolb  30846  hlimreui  31314  nmoplb  31982  nmfnlb  31999  dmdbr5ati  32497  disjunsn  32669  ind1a  32938  esplyind  33731  fsumcvg4  34107  issibf  34490  bnj1174  35159  derang0  35363  subfacp1lem6  35379  satfdm  35563  bj-denoteslem  37072  bj-rexcom4bv  37083  bj-rexcom4b  37084  bj-tagex  37188  bj-dfid2ALT  37266  bj-restuni  37302  rdgeqoa  37575  ftc1anclem5  37898  disjressuc2  38606  eqvrelcoss3  38885  dfeldisj5  38990  dibord  41429  eu6w  42929  ifpnot  43721  ifpdfxor  43738  ifpid1g  43745  ifpim1g  43752  ifpimimb  43755  relopabVD  45151  n0abso  45227  euabsneu  47284  rmotru  49058  reutru  49059