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  2574  eu6  2575  issettru  2815  issetlem  2817  rextru  3069  rexcom4b  3462  eueq  3655  ssrabeq  4025  nsspssun  4209  disjpss  4402  reusngf  4619  reuprg0  4647  reuprg  4648  pr1eqbg  4801  disjprg  5082  ax6vsep  5239  pwun  5518  dfid3  5523  elvv  5700  elvvv  5701  dfres3  5944  resopab  5994  xpcan2  6136  funfn  6523  dffn2  6665  dffn3  6675  dffn4  6753  fsn  7083  sucexb  7752  fparlem1  8056  ixp0x  8868  ac6sfi  9188  fiint  9231  rankc1  9788  cf0  10167  ind1a  12164  ccatrcan  14675  prmreclem2  16882  subislly  23459  ovoliunlem1  25482  plyun0  26175  dmcuts  27800  rightge0  27830  tgjustf  28558  ercgrg  28602  dfpth2  29815  0wlk  30204  0trl  30210  0pth  30213  0cycl  30222  nmoolb  30860  hlimreui  31328  nmoplb  31996  nmfnlb  32013  dmdbr5ati  32511  disjunsn  32682  esplyind  33737  fsumcvg4  34113  issibf  34496  bnj1174  35164  derang0  35370  subfacp1lem6  35386  satfdm  35570  bj-denoteslem  37197  bj-rexcom4bv  37208  bj-rexcom4b  37209  bj-tagex  37313  bj-dfid2ALT  37391  bj-restuni  37428  rdgeqoa  37703  ftc1anclem5  38035  disjressuc2  38749  eqvrelcoss3  39040  dfeldisj5  39151  dibord  41622  eu6w  43126  ifpnot  43918  ifpdfxor  43935  ifpid1g  43942  ifpim1g  43949  ifpimimb  43952  relopabVD  45348  n0abso  45424  euabsneu  47491  rmotru  49293  reutru  49294