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  2568  eu6  2569  issettru  2809  issetlem  2811  rextru  3063  rexcom4b  3468  eueq  3662  ssrabeq  4031  nsspssun  4215  disjpss  4408  reusngf  4624  reuprg0  4652  reuprg  4653  pr1eqbg  4806  disjprg  5085  ax6vsep  5239  pwun  5507  dfid3  5512  elvv  5689  elvvv  5690  dfres3  5932  resopab  5982  xpcan2  6124  funfn  6511  dffn2  6653  dffn3  6663  dffn4  6741  fsn  7068  sucexb  7737  fparlem1  8042  ixp0x  8850  ac6sfi  9168  fiint  9211  rankc1  9763  cf0  10142  ccatrcan  14626  prmreclem2  16829  subislly  23396  ovoliunlem1  25430  plyun0  26129  dmscut  27752  rightpos  27782  tgjustf  28451  ercgrg  28495  dfpth2  29707  0wlk  30096  0trl  30102  0pth  30105  0cycl  30114  nmoolb  30751  hlimreui  31219  nmoplb  31887  nmfnlb  31904  dmdbr5ati  32402  disjunsn  32574  ind1a  32840  fsumcvg4  33963  issibf  34346  bnj1174  35015  derang0  35213  subfacp1lem6  35229  satfdm  35413  bj-denoteslem  36915  bj-rexcom4bv  36926  bj-rexcom4b  36927  bj-tagex  37031  bj-dfid2ALT  37109  bj-restuni  37141  rdgeqoa  37414  ftc1anclem5  37747  disjressuc2  38445  eqvrelcoss3  38724  dfeldisj5  38829  dibord  41268  eu6w  42779  ifpnot  43573  ifpdfxor  43590  ifpid1g  43597  ifpim1g  43604  ifpimimb  43607  relopabVD  45003  n0abso  45079  euabsneu  47138  rmotru  48913  reutru  48914