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  3476  eueq  3676  ssrabeq  4043  nsspssun  4227  disjpss  4420  reusngf  4634  reuprg0  4662  reuprg  4663  pr1eqbg  4817  disjprg  5098  ax6vsep  5253  pwun  5524  dfid3  5529  elvv  5706  elvvv  5707  dfres3  5944  resopab  5994  xpcan2  6138  funfn  6530  dffn2  6672  dffn3  6682  dffn4  6760  fsn  7089  sucexb  7760  fparlem1  8068  ixp0x  8876  ac6sfi  9207  fiint  9253  fiintOLD  9254  rankc1  9799  cf0  10180  ccatrcan  14660  prmreclem2  16864  subislly  23401  ovoliunlem1  25436  plyun0  26135  dmscut  27757  tgjustf  28453  ercgrg  28497  dfpth2  29709  0wlk  30095  0trl  30101  0pth  30104  0cycl  30113  nmoolb  30750  hlimreui  31218  nmoplb  31886  nmfnlb  31903  dmdbr5ati  32401  disjunsn  32573  ind1a  32832  fsumcvg4  33933  issibf  34317  bnj1174  34986  derang0  35149  subfacp1lem6  35165  satfdm  35349  bj-denoteslem  36852  bj-rexcom4bv  36863  bj-rexcom4b  36864  bj-tagex  36968  bj-dfid2ALT  37046  bj-restuni  37078  rdgeqoa  37351  ftc1anclem5  37684  disjressuc2  38367  eqvrelcoss3  38602  dfeldisj5  38706  dibord  41146  eu6w  42657  ifpnot  43452  ifpdfxor  43469  ifpid1g  43476  ifpim1g  43483  ifpimimb  43486  relopabVD  44883  n0abso  44959  euabsneu  47022  rmotru  48784  reutru  48785