Theorem biantru 534

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  biantrur  535  pm4.71  562  eu6lem  2577  eu6  2578  issettru  2817  issetlem  2819  rextru  3070  rexcom4b  3462  eueq  3649  ssrabeq  4015  nsspssun  4196  disjpss  4389  reusngf  4606  reuprg0  4634  reuprg  4635  pr1eqbg  4788  disjprg  5068  ax6vsep  5225  pwun  5511  dfid3  5516  elvv  5693  elvvv  5694  dfres3  5936  resopab  5986  xpcan2  6128  funfn  6515  dffn2  6657  dffn3  6667  dffn4  6745  fsn  7077  sucexb  7747  fparlem1  8051  ixp0x  8864  ac6sfi  9184  fiint  9227  rankc1  9785  cf0  10164  ind1a  12161  ccatrcan  14672  prmreclem2  16879  subislly  23464  ovoliunlem1  25487  plyun0  26180  dmcuts  27801  rightge0  27831  tgjustf  28559  ercgrg  28603  dfpth2  29815  0wlk  30204  0trl  30210  0pth  30213  0cycl  30222  nmoolb  30860  hlimreui  31328  nmoplb  31996  nmfnlb  32013  dmdbr5ati  32511  disjunsn  32683  esplyind  33759  fsumcvg4  34134  issibf  34517  bnj1174  35185  derang0  35397  subfacp1lem6  35413  satfdm  35597  bj-denoteslem  37224  bj-rexcom4bv  37235  bj-rexcom4b  37236  bj-tagex  37340  bj-dfid2ALT  37418  bj-restuni  37455  rdgeqoa  37732  ftc1anclem5  38064  disjressuc2  38778  eqvrelcoss3  39069  dfeldisj5  39180  dibord  41651  eu6w  43126  ifpnot  43914  ifpdfxor  43931  ifpid1g  43938  ifpim1g  43945  ifpimimb  43948  relopabVD  45344  n0abso  45420  euabsneu  47491  rmotru  49293  reutru  49294