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  3468  eueq  3668  ssrabeq  4035  nsspssun  4219  disjpss  4412  reusngf  4626  reuprg0  4654  reuprg  4655  pr1eqbg  4808  disjprg  5088  ax6vsep  5242  pwun  5512  dfid3  5517  elvv  5694  elvvv  5695  dfres3  5935  resopab  5985  xpcan2  6126  funfn  6512  dffn2  6654  dffn3  6664  dffn4  6742  fsn  7069  sucexb  7740  fparlem1  8045  ixp0x  8853  ac6sfi  9173  fiint  9216  fiintOLD  9217  rankc1  9766  cf0  10145  ccatrcan  14625  prmreclem2  16829  subislly  23366  ovoliunlem1  25401  plyun0  26100  dmscut  27722  tgjustf  28418  ercgrg  28462  dfpth2  29674  0wlk  30060  0trl  30066  0pth  30069  0cycl  30078  nmoolb  30715  hlimreui  31183  nmoplb  31851  nmfnlb  31868  dmdbr5ati  32366  disjunsn  32538  ind1a  32802  fsumcvg4  33917  issibf  34301  bnj1174  34970  derang0  35146  subfacp1lem6  35162  satfdm  35346  bj-denoteslem  36849  bj-rexcom4bv  36860  bj-rexcom4b  36861  bj-tagex  36965  bj-dfid2ALT  37043  bj-restuni  37075  rdgeqoa  37348  ftc1anclem5  37681  disjressuc2  38364  eqvrelcoss3  38599  dfeldisj5  38703  dibord  41142  eu6w  42653  ifpnot  43447  ifpdfxor  43464  ifpid1g  43471  ifpim1g  43478  ifpimimb  43481  relopabVD  44878  n0abso  44954  euabsneu  47016  rmotru  48791  reutru  48792