Theorem biantru 790

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

Hypothesis

Ref	Expression
biantru.1	|- ph

Assertion

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

Proof of Theorem biantru

Step	Hyp	Ref	Expression
1		biantru.1	. 2 |- ph
2		iba 701	. 2 |- (ph -> (ps <-> (ps /\ ph)))
3	1, 2	ax-mp 7	1 |- (ps <-> (ps /\ ph))

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

This theorem is referenced by:  mpbiran2 796  hbsb4tOLD 1460  isset 2129  eueq 2260  nsspssun 2653  disjpss 2748  pwundif 3394  pwun 3395  dfid3 3402  posn 3418  eufromeq6 3644  sucexb 3701  elvv 3864  elvvv 3865  resopab 4063  dfima2OLD 4077  xpcan2 4161  xp11aOLD 4162  funfn 4262  dffn2 4374  dffn3 4381  dffn4 4434  f1orn 4459  fsn 4618  dfoprab2 4728  fparlem3 4894  ixp0x 5229  dom0 5339  mapdom2 5398  fiint 5460  rankc1 5625  cf0 5854  supsrlem5 6177  eltopsp 8668  islp2 8818  nmolb 9568  symgval 9995  symggrpi 9998  choc0 10715  nmoplb 11260  nmfnlb 11277  dmdbr5ati 11786  bnj512 12311  bnj1174 13234  isprm2 13567  wfrlem8 13756  rexcom4b 15342  elstrscaf 16475

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