Theorem biantrur 725

Description: A wff is equivalent to its conjunction with truth.

Hypothesis

Ref	Expression
biantrur.1	|- ph

Assertion

Ref	Expression
biantrur	|- (ps <-> (ph /\ ps))

Proof of Theorem biantrur

Step	Hyp	Ref	Expression
1		biantrur.1	. 2 |- ph
2		ibar 643	. 2 |- (ph -> (ps <-> (ph /\ ps)))
3	1, 2	ax-mp 7	1 |- (ps <-> (ph /\ ps))

Syntax hints:   <-> wb 146   /\ wa 223

This theorem is referenced by:  mpbiran 728  rexv 1821  euxfr 1927  ddif 2169  nssinpss 2240  nsspssun 2241  difab 2269  elimif 2374  xp11b 3478  ssrnres 3481  funcnv2 3556  fvopabg 3785  fvreseq 3799  fnressn 3837  abrexexlem2 3859  oprabval5 4029  fo1st 4091  fo2nd 4092  df1st2 4126  df2nd2 4127  fnmap 4329  mapvalg 4330  pmvalg 4331  elixp 4350  pw2en 4446  mapenlem2 4490  rankeq0 4696  cdavalt 4919  nnwos 6460  dfseq0 6563  absgt0 6843  isumclimtf 7195  infcvglem1 7221  isbasis3g 7613  opnssneib 7729  phoeqi 8518  spwval2 8653  shlesb1 9359  chnle 9408  pjnel 9668  hoeqt 9686  hoeq1t 9756  nmop0 9910  nmfn0 9911  cvexchlem 10295  dmdbr5at 10349

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain