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  2572  eu6  2573  issettru  2818  issetlem  2820  rextru  3076  rexcom4b  3512  eueq  3713  ssrabeq  4083  nsspssun  4267  disjpss  4460  reusngf  4673  reuprg0  4701  reuprg  4702  pr1eqbg  4856  disjprg  5138  ax6vsep  5302  pwun  5575  dfid3  5580  elvv  5759  elvvv  5760  dfres3  6001  resopab  6051  xpcan2  6196  funfn  6595  dffn2  6737  dffn3  6747  dffn4  6825  fsn  7154  sucexb  7825  fparlem1  8138  wfrlem8OLD  8357  ixp0x  8967  ac6sfi  9321  fiint  9367  fiintOLD  9368  rankc1  9911  cf0  10292  ccatrcan  14758  prmreclem2  16956  subislly  23490  ovoliunlem1  25538  plyun0  26237  dmscut  27857  tgjustf  28482  ercgrg  28526  dfpth2  29750  0wlk  30136  0trl  30142  0pth  30145  0cycl  30154  nmoolb  30791  hlimreui  31259  nmoplb  31927  nmfnlb  31944  dmdbr5ati  32442  disjunsn  32608  ind1a  32845  fsumcvg4  33950  issibf  34336  bnj1174  35018  derang0  35175  subfacp1lem6  35191  satfdm  35375  bj-denoteslem  36873  bj-rexcom4bv  36884  bj-rexcom4b  36885  bj-tagex  36989  bj-dfid2ALT  37067  bj-restuni  37099  rdgeqoa  37372  ftc1anclem5  37705  disjressuc2  38390  eqvrelcoss3  38620  dfeldisj5  38723  dibord  41162  eu6w  42691  ifpnot  43488  ifpdfxor  43505  ifpid1g  43512  ifpim1g  43519  ifpimimb  43522  relopabVD  44926  n0abso  44998  euabsneu  47045  rmotru  48728  reutru  48729