Theorem biantrur 544

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 487	. 2 |- (ph -> (ps <-> (ph /\ ps)))
3	1, 2	ax-mp 6	1 |- (ps <-> (ph /\ ps))

Syntax hints:   <-> wb 127   /\ wa 196

This theorem is referenced by:  mpbiran 547  rexv 1358  euxfr 1436  elabs2 1457  ddif 1597  nssinpss 1665  nsspssun 1666  difab 1693  disj2 1735  intmin2 1984  funcnv2 2702  fvopabg 2872  fvreseq 2882  fnressn 2897  abrexexlem2 2911  fo1st 3094  fo2nd 3095  1st2val 3097  df1st2 3098  fnmap 3262  mapvalg 3263  pw2en 3348  mapenlem2 3385  cdavalt 3716  nnwos 4610  seqval 4665  shlesb1 5360  chnle 5406  pjnel 5665  cvexchlem 5759

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org