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  2599  eu6  2600  issettru  2839  issetlem  2841  rextru  3094  rexcom4b  3482  eueq  3666  ssrabeq  4032  nsspssun  4214  disjpss  4414  reusngf  4635  reuprg0  4663  reuprg  4664  pr1eqbg  4817  disjprg  5099  ax6vsep  5257  pwun  5544  dfid3  5549  elvv  5726  elvvv  5727  dfres3  5975  resopab  6026  xpcan2  6169  funfn  6570  dffn2  6711  dffn3  6722  dffn4  6802  fsn  7136  sucexb  7818  fparlem1  8123  ixp0x  8954  ac6sfi  9275  fiint  9318  rankc1  9887  cf0  10328  ind1a  12331  ccatrcan  14868  prmreclem2  17095  subislly  23800  ovoliunlem1  25823  plyun0  26515  dmcuts  28177  rightge0  28207  tgjustf  28935  ercgrg  28980  dfpth2  30314  0wlk  30707  0trl  30713  0pth  30716  0cycl  30725  nmoolb  31373  hlimreui  31841  nmoplb  32509  nmfnlb  32526  dmdbr5ati  33024  disjunsn  33188  esplyind  34207  fsumcvg4  34582  issibf  34965  bnj1174  35633  derang0  35934  subfacp1lem6  35950  satfdm  36134  bj-denoteslem  37783  bj-rexcom4bv  37794  bj-rexcom4b  37795  bj-tagex  37900  coi1in  37961  bj-dfid2ALT  37980  bj-restuni  38018  rdgeqoa  38293  ftc1anclem5  38615  disjressuc2  39343  eqvrelcoss3  39634  dfeldisj5  39745  dibord  42216  eu6w  43687  ifpnot  44470  ifpdfxor  44487  ifpid1g  44494  ifpim1g  44501  ifpimimb  44504  relopabVD  45882  n0abso  45965  euabsneu  48097  rmotru  49912  reutru  49913