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  2567  eu6  2568  issettru  2807  issetlem  2809  rextru  3061  rexcom4b  3482  eueq  3682  ssrabeq  4050  nsspssun  4234  disjpss  4427  reusngf  4641  reuprg0  4669  reuprg  4670  pr1eqbg  4824  disjprg  5106  ax6vsep  5261  pwun  5534  dfid3  5539  elvv  5716  elvvv  5717  dfres3  5958  resopab  6008  xpcan2  6153  funfn  6549  dffn2  6693  dffn3  6703  dffn4  6781  fsn  7110  sucexb  7783  fparlem1  8094  ixp0x  8902  ac6sfi  9238  fiint  9284  fiintOLD  9285  rankc1  9830  cf0  10211  ccatrcan  14691  prmreclem2  16895  subislly  23375  ovoliunlem1  25410  plyun0  26109  dmscut  27730  tgjustf  28407  ercgrg  28451  dfpth2  29666  0wlk  30052  0trl  30058  0pth  30061  0cycl  30070  nmoolb  30707  hlimreui  31175  nmoplb  31843  nmfnlb  31860  dmdbr5ati  32358  disjunsn  32530  ind1a  32789  fsumcvg4  33947  issibf  34331  bnj1174  35000  derang0  35163  subfacp1lem6  35179  satfdm  35363  bj-denoteslem  36866  bj-rexcom4bv  36877  bj-rexcom4b  36878  bj-tagex  36982  bj-dfid2ALT  37060  bj-restuni  37092  rdgeqoa  37365  ftc1anclem5  37698  disjressuc2  38381  eqvrelcoss3  38616  dfeldisj5  38720  dibord  41160  eu6w  42671  ifpnot  43466  ifpdfxor  43483  ifpid1g  43490  ifpim1g  43497  ifpimimb  43500  relopabVD  44897  n0abso  44973  euabsneu  47033  rmotru  48795  reutru  48796