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

Theorem biantru 526
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 524 . 2 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  pm4.71  661  mpbiran2  953  isset  3196  rexcom4b  3216  rabtru  3348  eueq  3364  ssrabeq  3672  nsspssun  3840  disjpss  4005  pr1eqbg  4363  disjprg  4613  ax6vsep  4750  pwun  4987  dfid3  4995  elvv  5143  elvvv  5144  resopab  5410  xpcan2  5535  funfn  5882  dffn2  6009  dffn3  6016  dffn4  6083  fsn  6362  sucexb  6963  fparlem1  7229  fsplit  7234  wfrlem8  7374  ixp0x  7888  ac6sfi  8156  fiint  8189  rankc1  8685  cf0  9025  ccatrcan  13419  prmreclem2  15556  subislly  21207  ovoliunlem1  23193  plyun0  23874  ercgrg  25329  0wlk  26860  0trl  26866  0pth  26869  0cycl  26877  nmoolb  27496  hlimreui  27966  nmoplb  28636  nmfnlb  28653  dmdbr5ati  29151  disjunsn  29275  fsumcvg4  29802  ind1a  29888  issibf  30200  bnj1174  30814  derang0  30894  subfacp1lem6  30910  dfres3  31392  bj-denotes  32540  bj-rexcom4bv  32553  bj-rexcom4b  32554  bj-tagex  32657  bj-restuni  32722  rdgeqoa  32885  ftc1anclem5  33156  dibord  35963  ifpnot  37330  ifpdfxor  37348  ifpid1g  37355  ifpim1g  37362  ifpimimb  37365  relopabVD  38655  funressnfv  40538
  Copyright terms: Public domain W3C validator