Theorem biantru 539

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  biantrur  540  pm4.71  567  eu6lem  2604  eu6  2605  issettru  2844  issetlem  2846  rextru  3099  rexcom4b  3489  eueq  3674  ssrabeq  4041  nsspssun  4224  disjpss  4424  reusngf  4645  reuprg0  4673  reuprg  4674  pr1eqbg  4827  disjprg  5110  ax6vsep  5271  pwun  5559  dfid3  5564  elvv  5741  elvvv  5742  dfres3  5988  resopab  6041  xpcan2  6180  funfn  6573  dffn2  6714  dffn3  6725  dffn4  6805  fsn  7138  sucexb  7812  fparlem1  8116  ixp0x  8933  ac6sfi  9254  fiint  9296  rankc1  9852  cf0  10252  ind1a  12247  ccatrcan  14780  prmreclem2  17002  subislly  23675  ovoliunlem1  25698  plyun0  26391  dmcuts  28021  rightge0  28051  tgjustf  28779  ercgrg  28823  dfpth2  30115  0wlk  30504  0trl  30510  0pth  30513  0cycl  30522  nmoolb  31160  hlimreui  31628  nmoplb  32296  nmfnlb  32313  dmdbr5ati  32811  disjunsn  32976  esplyind  33996  fsumcvg4  34371  issibf  34754  bnj1174  35422  derang0  35681  subfacp1lem6  35697  satfdm  35881  bj-denoteslem  37546  bj-rexcom4bv  37557  bj-rexcom4b  37558  bj-tagex  37663  bj-dfid2ALT  37741  bj-restuni  37779  rdgeqoa  38056  ftc1anclem5  38388  disjressuc2  39100  eqvrelcoss3  39391  dfeldisj5  39502  dibord  41973  eu6w  43448  ifpnot  44236  ifpdfxor  44253  ifpid1g  44260  ifpim1g  44267  ifpimimb  44270  relopabVD  45649  n0abso  45725  euabsneu  47805  rmotru  49621  reutru  49622