Theorem biantrur 723

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 641	. 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 726  rexv 1812  euxfr 1917  ddif 2159  nssinpss 2230  nsspssun 2231  difab 2259  elimif 2364  ssrnres 3467  funcnv2 3542  fvopabg 3770  fvreseq 3784  fnressn 3822  abrexexlem2 3844  oprabval5 4014  fo1st 4075  fo2nd 4076  df1st2 4110  df2nd2 4111  fnmap 4313  mapvalg 4314  pmvalg 4315  elixp 4334  pw2en 4426  mapenlem2 4470  rankeq0 4668  cdavalt 4891  nnwos 6392  dfseq0 6495  isumclimtf 7131  infcvglem1 7156  isbasis3g 7555  opnssneib 7670  phoeqi 8449  spwval2 8577  shlesb1 9274  chnle 9323  pjnel 9585  hoeqt 9603  hoeq1t 9673  nmop0 9826  nmfn0 9827  cvexchlem 10203  dmdbr5at 10255

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