Theorem biantru 525

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

Syntax hints:   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  pm4.71  663  mpbiran2  974  isset  3238  rexcom4b  3258  rabtru  3393  eueq  3411  ssrabeq  3722  nsspssun  3890  disjpss  4061  pr1eqbg  4421  disjprg  4680  ax6vsep  4818  pwun  5051  dfid3  5054  elvv  5211  elvvv  5212  dfres3  5433  resopab  5481  xpcan2  5606  funfn  5956  dffn2  6085  dffn3  6092  dffn4  6159  fsn  6442  sucexb  7051  fparlem1  7322  fsplit  7327  wfrlem8  7467  ixp0x  7978  ac6sfi  8245  fiint  8278  rankc1  8771  cf0  9111  ccatrcan  13519  prmreclem2  15668  subislly  21332  ovoliunlem1  23316  plyun0  23998  ercgrg  25457  0wlk  27094  0trl  27100  0pth  27103  0cycl  27112  nmoolb  27754  hlimreui  28224  nmoplb  28894  nmfnlb  28911  dmdbr5ati  29409  disjunsn  29533  fsumcvg4  30124  ind1a  30209  issibf  30523  bnj1174  31197  derang0  31277  subfacp1lem6  31293  dmscut  32043  bj-denotes  32983  bj-rexcom4bv  32996  bj-rexcom4b  32997  bj-tagex  33100  bj-restuni  33175  bj-ismooredr2  33190  rdgeqoa  33348  ftc1anclem5  33619  dibord  36765  ifpnot  38131  ifpdfxor  38149  ifpid1g  38156  ifpim1g  38163  ifpimimb  38166  relopabVD  39451  funressnfv  41529