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  2573  eu6  2574  issettru  2813  issetlem  2815  rextru  3068  rexcom4b  3497  eueq  3696  ssrabeq  4064  nsspssun  4248  disjpss  4441  reusngf  4655  reuprg0  4683  reuprg  4684  pr1eqbg  4838  disjprg  5120  ax6vsep  5278  pwun  5551  dfid3  5556  elvv  5734  elvvv  5735  dfres3  5976  resopab  6026  xpcan2  6171  funfn  6571  dffn2  6713  dffn3  6723  dffn4  6801  fsn  7130  sucexb  7803  fparlem1  8116  wfrlem8OLD  8335  ixp0x  8945  ac6sfi  9297  fiint  9343  fiintOLD  9344  rankc1  9889  cf0  10270  ccatrcan  14742  prmreclem2  16942  subislly  23424  ovoliunlem1  25460  plyun0  26159  dmscut  27780  tgjustf  28457  ercgrg  28501  dfpth2  29716  0wlk  30102  0trl  30108  0pth  30111  0cycl  30120  nmoolb  30757  hlimreui  31225  nmoplb  31893  nmfnlb  31910  dmdbr5ati  32408  disjunsn  32580  ind1a  32841  fsumcvg4  33986  issibf  34370  bnj1174  35039  derang0  35196  subfacp1lem6  35212  satfdm  35396  bj-denoteslem  36894  bj-rexcom4bv  36905  bj-rexcom4b  36906  bj-tagex  37010  bj-dfid2ALT  37088  bj-restuni  37120  rdgeqoa  37393  ftc1anclem5  37726  disjressuc2  38411  eqvrelcoss3  38641  dfeldisj5  38744  dibord  41183  eu6w  42666  ifpnot  43461  ifpdfxor  43478  ifpid1g  43485  ifpim1g  43492  ifpimimb  43495  relopabVD  44892  n0abso  44968  euabsneu  47024  rmotru  48749  reutru  48750