Theorem biantrur 727

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 645	. 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 730  rexv 1824  euxfr 1930  ddif 2173  nssinpss 2244  nsspssun 2245  difab 2273  elimif 2379  xp11b 3485  ssrnres 3488  funcnv2 3563  fvopabg 3792  fvreseq 3806  fnressn 3844  abrexexlem2 3866  oprabval5 4036  fo1st 4098  fo2nd 4099  df1st2 4133  df2nd2 4134  fnmap 4336  mapvalg 4337  pmvalg 4338  elixp 4357  pw2en 4453  mapenlem2 4497  rankeq0 4713  cdavalt 4938  nnwos 6468  dfseq0 6571  absgt0 6850  isumclimtf 7202  infcvglem1 7228  isbasis3g 7619  opnssneib 7733  phoeqi 8521  spwval2 8656  shlesb1 9361  chnle 9410  pjnel 9670  hoeqt 9688  hoeq1t 9758  nmop0 9912  nmfn0 9913  cvexchlem 10298  dmdbr5at 10352

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