Theorem biantrur 791

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

Syntax hints:   <-> wb 162   /\ wa 239

This theorem is referenced by:  mpbiran 795  rexv 2139  reuv 2140  rabab 2141  euxfr 2271  euind 2272  ddif 2569  nssinpss 2651  nssinpssOLD 2652  nsspssun 2653  difabOLD 2690  vss 2732  elimif 2825  eualeqhb 3635  euexeqOLD 3637  euexaleq 3638  eufromeq2 3640  intirr 4123  xpcan 4159  xp11bOLD 4160  ssrnres 4165  dfco2aOLD 4206  funcnv2 4285  fvopabg 4559  eqfnfv2 4578  fnressn 4623  abrexexlem2 4646  oprabval5 4769  fo1st 4843  fo2nd 4844  df1st2 4879  df2nd2 4880  fparlem1 4892  fparlem2 4893  fparlem4 4895  frsucmpt 4974  fnmap 5199  mapvalg 5200  pmvalg 5201  elixp 5220  riotav 5376  rankeq0 5616  cdaval 5863  nnwos 7424  dfseq0 7601  absgt0i 7889  hashgval 8025  isumclimtfi 8251  infcvglem1 8277  isbasis3g 8677  opnssneib 8800  spwval2 9791  dford2 9973  filmapf 10099  shlesb1i 10784  chnlei 10833  pjneli 11095  nmop0 11339  nmfn0 11340  cvexchlem 11732  dmdbr5ati 11786  bnj22 12983  bnj53 12985  fz1eqblem 13400  gcd0id 13521  mulgcdlem2 13549  zgt1b2 13564  elpotr 13638  axfelem9 13829  sallnei 14594  neibastop2lem3 15203  neibastop2lem4 15204  compel 16097  glb0 16675

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 163  df-an 241

Copyright terms: Public domain