Theorem biantru 538

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  biantrur  539  pm4.71  566  eu6lem  2601  eu6  2602  issettru  2841  issetlem  2843  rextru  3096  rexcom4b  3486  eueq  3671  ssrabeq  4038  nsspssun  4221  disjpss  4421  reusngf  4640  reuprg0  4668  reuprg  4669  pr1eqbg  4822  disjprg  5105  ax6vsep  5266  pwun  5554  dfid3  5559  elvv  5736  elvvv  5737  dfres3  5983  resopab  6036  xpcan2  6175  funfn  6566  dffn2  6707  dffn3  6718  dffn4  6798  fsn  7131  sucexb  7799  fparlem1  8103  ixp0x  8920  ac6sfi  9240  fiint  9282  rankc1  9838  cf0  10229  ind1a  12224  ccatrcan  14752  prmreclem2  16972  subislly  23638  ovoliunlem1  25661  plyun0  26354  dmcuts  27984  rightge0  28014  tgjustf  28742  ercgrg  28786  dfpth2  30078  0wlk  30467  0trl  30473  0pth  30476  0cycl  30485  nmoolb  31123  hlimreui  31591  nmoplb  32259  nmfnlb  32276  dmdbr5ati  32774  disjunsn  32939  esplyind  33965  fsumcvg4  34340  issibf  34723  bnj1174  35391  derang0  35661  subfacp1lem6  35677  satfdm  35861  bj-denoteslem  37526  bj-rexcom4bv  37537  bj-rexcom4b  37538  bj-tagex  37643  bj-dfid2ALT  37721  bj-restuni  37759  rdgeqoa  38036  ftc1anclem5  38368  disjressuc2  39080  eqvrelcoss3  39371  dfeldisj5  39482  dibord  41953  eu6w  43428  ifpnot  44216  ifpdfxor  44233  ifpid1g  44240  ifpim1g  44247  ifpimimb  44250  relopabVD  45629  n0abso  45705  euabsneu  47785  rmotru  49601  reutru  49602