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  3068  rexcom4b  3461  eueq  3654  ssrabeq  4024  nsspssun  4208  disjpss  4401  reusngf  4618  reuprg0  4646  reuprg  4647  pr1eqbg  4800  disjprg  5081  ax6vsep  5238  pwun  5524  dfid3  5529  elvv  5706  elvvv  5707  dfres3  5949  resopab  5999  xpcan2  6141  funfn  6528  dffn2  6670  dffn3  6680  dffn4  6758  fsn  7088  sucexb  7758  fparlem1  8062  ixp0x  8874  ac6sfi  9194  fiint  9237  rankc1  9794  cf0  10173  ind1a  12170  ccatrcan  14681  prmreclem2  16888  subislly  23446  ovoliunlem1  25469  plyun0  26162  dmcuts  27783  rightge0  27813  tgjustf  28541  ercgrg  28585  dfpth2  29797  0wlk  30186  0trl  30192  0pth  30195  0cycl  30204  nmoolb  30842  hlimreui  31310  nmoplb  31978  nmfnlb  31995  dmdbr5ati  32493  disjunsn  32664  esplyind  33719  fsumcvg4  34094  issibf  34477  bnj1174  35145  derang0  35351  subfacp1lem6  35367  satfdm  35551  bj-denoteslem  37178  bj-rexcom4bv  37189  bj-rexcom4b  37190  bj-tagex  37294  bj-dfid2ALT  37372  bj-restuni  37409  rdgeqoa  37686  ftc1anclem5  38018  disjressuc2  38732  eqvrelcoss3  39023  dfeldisj5  39134  dibord  41605  eu6w  43109  ifpnot  43897  ifpdfxor  43914  ifpid1g  43921  ifpim1g  43928  ifpimimb  43931  relopabVD  45327  n0abso  45403  euabsneu  47476  rmotru  49278  reutru  49279