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  2566  eu6  2567  issettru  2806  issetlem  2808  rextru  3060  rexcom4b  3479  eueq  3679  ssrabeq  4047  nsspssun  4231  disjpss  4424  reusngf  4638  reuprg0  4666  reuprg  4667  pr1eqbg  4821  disjprg  5103  ax6vsep  5258  pwun  5531  dfid3  5536  elvv  5713  elvvv  5714  dfres3  5955  resopab  6005  xpcan2  6150  funfn  6546  dffn2  6690  dffn3  6700  dffn4  6778  fsn  7107  sucexb  7780  fparlem1  8091  ixp0x  8899  ac6sfi  9231  fiint  9277  fiintOLD  9278  rankc1  9823  cf0  10204  ccatrcan  14684  prmreclem2  16888  subislly  23368  ovoliunlem1  25403  plyun0  26102  dmscut  27723  tgjustf  28400  ercgrg  28444  dfpth2  29659  0wlk  30045  0trl  30051  0pth  30054  0cycl  30063  nmoolb  30700  hlimreui  31168  nmoplb  31836  nmfnlb  31853  dmdbr5ati  32351  disjunsn  32523  ind1a  32782  fsumcvg4  33940  issibf  34324  bnj1174  34993  derang0  35156  subfacp1lem6  35172  satfdm  35356  bj-denoteslem  36859  bj-rexcom4bv  36870  bj-rexcom4b  36871  bj-tagex  36975  bj-dfid2ALT  37053  bj-restuni  37085  rdgeqoa  37358  ftc1anclem5  37691  disjressuc2  38374  eqvrelcoss3  38609  dfeldisj5  38713  dibord  41153  eu6w  42664  ifpnot  43459  ifpdfxor  43476  ifpid1g  43483  ifpim1g  43490  ifpimimb  43493  relopabVD  44890  n0abso  44966  euabsneu  47029  rmotru  48791  reutru  48792