MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biantru Structured version   Visualization version   GIF version

Theorem biantru 530
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
biantru.1 𝜑
Assertion
Ref Expression
biantru (𝜓 ↔ (𝜓𝜑))

Proof of Theorem biantru
StepHypRef Expression
1 biantru.1 . 2 𝜑
2 iba 528 . 2 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  biantrur  531  pm4.71  558  eu6lem  2656  eu6  2657  isset  3512  rexcom4b  3530  eueq  3703  ssrabeq  4063  nsspssun  4238  disjpss  4413  reusngf  4611  reuprg0  4637  reuprg  4638  pr1eqbg  4786  disjprgw  5058  disjprg  5059  ax6vsep  5204  pwun  5457  dfid3  5461  elvv  5625  elvvv  5626  dfres3  5857  resopab  5901  xpcan2  6032  funfn  6382  dffn2  6513  dffn3  6522  dffn4  6593  fsn  6893  sucexb  7512  fparlem1  7798  fsplitOLD  7804  wfrlem8  7953  ixp0x  8479  ac6sfi  8751  fiint  8784  rankc1  9288  cf0  9662  ccatrcan  14071  prmreclem2  16243  subislly  22005  ovoliunlem1  24018  plyun0  24702  tgjustf  26173  ercgrg  26217  0wlk  27809  0trl  27815  0pth  27818  0cycl  27827  nmoolb  28462  hlimreui  28930  nmoplb  29598  nmfnlb  29615  dmdbr5ati  30113  disjunsn  30259  fsumcvg4  31079  ind1a  31164  issibf  31477  bnj1174  32159  derang0  32300  subfacp1lem6  32316  satfdm  32500  dmscut  33156  bj-denotes  34072  bj-rexcom4bv  34082  bj-rexcom4b  34083  bj-tagex  34183  bj-restuni  34269  rdgeqoa  34520  ftc1anclem5  34838  eqvrelcoss3  35720  dfeldisj5  35821  dibord  38162  ifpnot  39700  ifpdfxor  39718  ifpid1g  39725  ifpim1g  39732  ifpimimb  39735  relopabVD  41100  euabsneu  43129
  Copyright terms: Public domain W3C validator