Theorem biantru 527

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

Syntax hints:   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  pm4.71  555  mpbiran2  703  eu6lem  2644  eu6OLD  2647  isset  3424  rexcom4b  3444  rabtru  3582  eueq  3602  eueqOLD  3603  ssrabeq  3915  nsspssun  4087  disjpss  4252  pr1eqbg  4605  disjprg  4869  ax6vsep  5009  pwun  5248  dfid3  5251  elvv  5410  elvvv  5411  dfres3  5634  resopab  5683  xpcan2  5812  funfn  6153  dffn2  6280  dffn3  6289  dffn4  6359  fsn  6652  sucexb  7270  fparlem1  7541  fsplit  7546  wfrlem8  7688  ixp0x  8203  ac6sfi  8473  fiint  8506  rankc1  9010  cf0  9388  ccatrcan  13808  prmreclem2  15992  subislly  21655  ovoliunlem1  23668  plyun0  24352  tgjustf  25785  ercgrg  25829  0wlk  27492  0trl  27498  0pth  27501  0cycl  27510  nmoolb  28181  hlimreui  28651  nmoplb  29321  nmfnlb  29338  dmdbr5ati  29836  disjunsn  29954  fsumcvg4  30541  ind1a  30626  issibf  30940  bnj1174  31617  derang0  31697  subfacp1lem6  31713  dmscut  32457  bj-denotes  33377  bj-rexcom4bv  33391  bj-rexcom4b  33392  bj-tagex  33497  bj-restuni  33573  bj-ismooredr2  33588  rdgeqoa  33763  ftc1anclem5  34032  eqvrelcoss3  34907  dibord  37234  ifpnot  38656  ifpdfxor  38674  ifpid1g  38681  ifpim1g  38688  ifpimimb  38691  relopabVD  39955  euabsneu  41964