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

Theorem biantrur 526
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 . 2 𝜑
2 ibar 524 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  mpbiran  955  cases  1004  truan  1492  2sb5rf  2439  rexv  3193  reuv  3194  rmov  3195  rabab  3196  euxfr  3359  euind  3360  ddif  3704  nssinpss  3818  nsspssun  3819  vss  3964  difsnpss  4279  sspr  4306  sstp  4307  disjprg  4578  mptv  4679  reusv2lem5  4799  oteqex2  4888  dfid4  4955  intirr  5433  xpcan  5489  fvopab6  6218  fnressn  6330  riotav  6516  mpt2v  6648  sorpss  6840  fparlem2  7165  fnsuppres  7209  brtpos0  7246  sup0riota  8254  genpass  9710  nnwos  11631  hashbclem  13093  ccatlcan  13324  clim0  14085  gcd0id  15078  pjfval2  19872  mat1dimbas  20097  pmatcollpw2lem  20401  isbasis3g  20564  opnssneib  20729  ssidcn  20869  qtopcld  21326  mdegleb  23628  vieta1  23871  lgsne0  24860  axpasch  25621  0wlk  26075  0trl  26076  shlesb1i  27629  chnlei  27728  pjneli  27966  cvexchlem  28611  dmdbr5ati  28665  elimifd  28746  lmxrge0  29326  cntnevol  29618  bnj110  30182  elpotr  30930  nofulllem1  31101  dfbigcup2  31176  bj-rexvwv  32060  bj-rababwv  32061  bj-sspwpwab  32239  finxpreclem4  32407  wl-cases2-dnf  32474  cnambfre  32628  lub0N  33494  glb0N  33498  cvlsupr3  33649  isdomn3  36801  ifpdfor2  36824  ifpdfor  36828  ifpim1  36832  ifpid2  36834  ifpim2  36835  ifpid2g  36857  ifpid1g  36858  ifpim23g  36859  ifpim1g  36865  ifpimimb  36868  rp-isfinite6  36883  rababg  36898  relnonrel  36912  rp-imass  37085  dffrege115  37292  opabn1stprc  40318  01wlk  41284
  Copyright terms: Public domain W3C validator