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

Theorem biantru 521
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 519 . 2 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 197  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 198  df-an 385
This theorem is referenced by:  pm4.71  549  mpbiran2  692  eu6  2645  isset  3412  rexcom4b  3432  rabtru  3567  eueq  3586  eueqOLD  3587  ssrabeq  3898  nsspssun  4070  disjpss  4236  pr1eqbg  4588  disjprg  4851  ax6vsep  4990  pwun  5228  dfid3  5231  elvv  5388  elvvv  5389  dfres3  5613  resopab  5662  xpcan2  5793  funfn  6138  dffn2  6265  dffn3  6274  dffn4  6344  fsn  6632  sucexb  7246  fparlem1  7518  fsplit  7523  wfrlem8  7665  ixp0x  8180  ac6sfi  8450  fiint  8483  rankc1  8987  cf0  9365  ccatrcan  13704  prmreclem2  15845  subislly  21506  ovoliunlem1  23493  plyun0  24177  ercgrg  25636  0wlk  27299  0trl  27305  0pth  27308  0cycl  27317  nmoolb  27964  hlimreui  28434  nmoplb  29104  nmfnlb  29121  dmdbr5ati  29619  disjunsn  29742  fsumcvg4  30331  ind1a  30416  issibf  30730  bnj1174  31403  derang0  31483  subfacp1lem6  31499  dmscut  32248  bj-denotes  33171  bj-rexcom4bv  33185  bj-rexcom4b  33186  bj-tagex  33291  bj-restuni  33367  bj-ismooredr2  33382  rdgeqoa  33540  ftc1anclem5  33807  dibord  36945  ifpnot  38319  ifpdfxor  38337  ifpid1g  38344  ifpim1g  38351  ifpimimb  38354  relopabVD  39636  euabsneu  41657  funressnfv  41667
  Copyright terms: Public domain W3C validator