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

Theorem biantrur 532
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
Hypothesis
Ref Expression
biantrur.1 𝜑
Assertion
Ref Expression
biantrur (𝜓 ↔ (𝜑𝜓))

Proof of Theorem biantrur
StepHypRef Expression
1 biantrur.1 . . 3 𝜑
21biantru 531 . 2 (𝜓 ↔ (𝜓𝜑))
32biancomi 464 1 (𝜓 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  mpbiran  708  cases  1042  truan  1553  2sb5rf  2471  euae  2656  rexv  3472  reuv  3473  rmov  3474  rabab  3475  euxfrw  3683  euxfr  3685  euind  3686  dfdif3  4078  ddif  4100  nssinpss  4220  nsspssun  4221  notabw  4267  vss  4407  reuprg0  4667  reuprg  4668  difsnpss  4771  sspr  4797  sstp  4798  disjprgw  5104  disjprg  5105  mptv  5225  reusv2lem5  5361  oteqex2  5460  dfid4  5536  intirr  6076  xpcan  6132  resssxp  6226  fvopab6  6985  fnressn  7108  riotav  7322  mpov  7472  sorpss  7669  opabn1stprc  7994  fparlem2  8049  fnsuppres  8126  brtpos0  8168  naddrid  8633  sup0riota  9409  genpass  10953  nnwos  12848  hashbclem  14358  ccatlcan  14615  clim0  15397  gcd0id  16407  pjfval2  21138  mat1dimbas  21844  pmatcollpw2lem  22149  isbasis3g  22322  opnssneib  22489  ssidcn  22629  qtopcld  23087  mdegleb  25452  vieta1  25695  lgsne0  26706  axpasch  27939  0wlk  29109  0clwlk  29123  shlesb1i  30377  chnlei  30476  pjneli  30714  cvexchlem  31359  dmdbr5ati  31413  elimifd  31515  lmxrge0  32597  cntnevol  32891  bnj110  33534  goeleq12bg  34007  fmlafvel  34043  elpotr  34419  dfbigcup2  34537  bj-rexvw  35400  bj-rababw  35401  bj-brab2a1  35670  finxpreclem4  35915  wl-cases2-dnf  36021  wl-euae  36026  wl-dfclab  36098  cnambfre  36176  triantru3  36735  lub0N  37701  glb0N  37705  cvlsupr3  37856  isdomn3  41578  ifpdfor2  41825  ifpdfor  41829  ifpim1  41833  ifpid2  41835  ifpim2  41836  ifpid2g  41857  ifpid1g  41858  ifpim23g  41859  ifpim1g  41865  ifpimimb  41868  rp-isfinite6  41882  rababg  41938  relnonrel  41951  dffrege115  42342  funressnfv  45367  dfnelbr2  45595
  Copyright terms: Public domain W3C validator