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  2570  eu6  2571  issettru  2811  issetlem  2813  rextru  3065  rexcom4b  3470  eueq  3664  ssrabeq  4035  nsspssun  4219  disjpss  4412  reusngf  4628  reuprg0  4656  reuprg  4657  pr1eqbg  4810  disjprg  5091  ax6vsep  5245  pwun  5514  dfid3  5519  elvv  5696  elvvv  5697  dfres3  5940  resopab  5990  xpcan2  6132  funfn  6519  dffn2  6661  dffn3  6671  dffn4  6749  fsn  7077  sucexb  7746  fparlem1  8051  ixp0x  8859  ac6sfi  9178  fiint  9221  rankc1  9773  cf0  10152  ccatrcan  14636  prmreclem2  16839  subislly  23406  ovoliunlem1  25440  plyun0  26139  dmscut  27762  rightpos  27792  tgjustf  28461  ercgrg  28505  dfpth2  29718  0wlk  30107  0trl  30113  0pth  30116  0cycl  30125  nmoolb  30762  hlimreui  31230  nmoplb  31898  nmfnlb  31915  dmdbr5ati  32413  disjunsn  32585  ind1a  32851  fsumcvg4  33974  issibf  34357  bnj1174  35026  derang0  35224  subfacp1lem6  35240  satfdm  35424  bj-denoteslem  36926  bj-rexcom4bv  36937  bj-rexcom4b  36938  bj-tagex  37042  bj-dfid2ALT  37120  bj-restuni  37152  rdgeqoa  37425  ftc1anclem5  37747  disjressuc2  38445  eqvrelcoss3  38724  dfeldisj5  38829  dibord  41268  eu6w  42784  ifpnot  43577  ifpdfxor  43594  ifpid1g  43601  ifpim1g  43608  ifpimimb  43611  relopabVD  45007  n0abso  45083  euabsneu  47142  rmotru  48917  reutru  48918