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  2576  eu6  2577  issettru  2822  issetlem  2824  rextru  3083  rexcom4b  3521  eueq  3730  ssrabeq  4107  nsspssun  4287  disjpss  4484  reusngf  4696  reuprg0  4727  reuprg  4728  pr1eqbg  4881  disjprg  5162  ax6vsep  5321  pwun  5591  dfid3  5596  elvv  5774  elvvv  5775  dfres3  6014  resopab  6063  xpcan2  6208  funfn  6608  dffn2  6749  dffn3  6759  dffn4  6840  fsn  7169  sucexb  7840  fparlem1  8153  wfrlem8OLD  8372  ixp0x  8984  ac6sfi  9348  fiint  9394  fiintOLD  9395  rankc1  9939  cf0  10320  ccatrcan  14767  prmreclem2  16964  subislly  23510  ovoliunlem1  25556  plyun0  26256  dmscut  27874  tgjustf  28499  ercgrg  28543  0wlk  30148  0trl  30154  0pth  30157  0cycl  30166  nmoolb  30803  hlimreui  31271  nmoplb  31939  nmfnlb  31956  dmdbr5ati  32454  disjunsn  32616  fsumcvg4  33896  ind1a  33983  issibf  34298  bnj1174  34979  derang0  35137  subfacp1lem6  35153  satfdm  35337  bj-denoteslem  36837  bj-rexcom4bv  36848  bj-rexcom4b  36849  bj-tagex  36953  bj-dfid2ALT  37031  bj-restuni  37063  rdgeqoa  37336  ftc1anclem5  37657  disjressuc2  38344  eqvrelcoss3  38574  dfeldisj5  38677  dibord  41116  eu6w  42631  ifpnot  43432  ifpdfxor  43449  ifpid1g  43456  ifpim1g  43463  ifpimimb  43466  relopabVD  44872  euabsneu  46943  rmotru  48536  reutru  48537