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

Theorem biantrur 522
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 520 . 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:  mpbiran  691  cases  1056  truan  1649  2sb5rf  2611  rexv  3412  reuv  3413  rmov  3414  rabab  3415  euxfr  3588  euind  3589  dfdif3  3917  ddif  3939  nssinpss  4056  nsspssun  4057  vss  4208  difsnpss  4526  sspr  4552  sstp  4553  disjprg  4838  mptv  4943  reusv2lem5  5069  oteqex2  5150  dfid4  5219  intirr  5723  xpcan  5779  fvopab6  6530  fnressn  6647  riotav  6838  mpt2v  6978  sorpss  7170  opabn1stprc  7458  fparlem2  7510  fnsuppres  7555  brtpos0  7592  sup0riota  8608  genpass  10114  nnwos  11972  hashbclem  13451  ccatlcan  13694  clim0  14458  gcd0id  15457  pjfval2  20261  mat1dimbas  20487  pmatcollpw2lem  20793  isbasis3g  20965  opnssneib  21131  ssidcn  21271  qtopcld  21728  mdegleb  24036  vieta1  24279  lgsne0  25272  axpasch  26033  0wlk  27287  0clwlk  27301  shlesb1i  28571  chnlei  28670  pjneli  28908  cvexchlem  29553  dmdbr5ati  29607  elimifd  29685  lmxrge0  30321  cntnevol  30614  bnj110  31249  elpotr  32004  dfbigcup2  32325  bj-cleljustab  33157  bj-rexvwv  33172  bj-rababwv  33173  finxpreclem4  33545  wl-cases2-dnf  33609  cnambfre  33768  triantru3  34319  lub0N  34967  glb0N  34971  cvlsupr3  35122  isdomn3  38281  ifpdfor2  38303  ifpdfor  38307  ifpim1  38311  ifpid2  38313  ifpim2  38314  ifpid2g  38336  ifpid1g  38337  ifpim23g  38338  ifpim1g  38344  ifpimimb  38347  rp-isfinite6  38362  rababg  38377  relnonrel  38391  rp-imass  38563  dffrege115  38770  dfnelbr2  41860
  Copyright terms: Public domain W3C validator