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

Theorem biantrur 534
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 533 . 2 (𝜓 ↔ (𝜓𝜑))
32biancomi 466 1 (𝜓 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  mpbiran  708  cases  1038  truan  1549  2sb5rf  2488  euae  2725  rexv  3470  reuv  3471  rmov  3472  rabab  3473  euxfrw  3663  euxfr  3665  euind  3666  dfdif3  4045  ddif  4067  nssinpss  4186  nsspssun  4187  vss  4354  reuprg0  4601  reuprg  4602  difsnpss  4703  sspr  4729  sstp  4730  disjprgw  5028  disjprg  5029  mptv  5138  reusv2lem5  5271  oteqex2  5357  dfid4  5429  intirr  5949  xpcan  6004  resssxp  6093  fvopab6  6782  fnressn  6901  riotav  7102  mpov  7247  sorpss  7438  opabn1stprc  7742  fparlem2  7795  fnsuppres  7844  brtpos0  7886  sup0riota  8917  genpass  10424  nnwos  12307  hashbclem  13810  ccatlcan  14075  clim0  14859  gcd0id  15861  pjfval2  20402  mat1dimbas  21081  pmatcollpw2lem  21386  isbasis3g  21558  opnssneib  21724  ssidcn  21864  qtopcld  22322  mdegleb  24669  vieta1  24912  lgsne0  25923  axpasch  26739  0wlk  27905  0clwlk  27919  shlesb1i  29173  chnlei  29272  pjneli  29510  cvexchlem  30155  dmdbr5ati  30209  elimifd  30314  lmxrge0  31309  cntnevol  31601  bnj110  32244  goeleq12bg  32710  fmlafvel  32746  elpotr  33140  dfbigcup2  33474  bj-rexvw  34321  bj-rababw  34322  bj-brab2a1  34565  finxpreclem4  34812  wl-cases2-dnf  34916  wl-euae  34921  wl-dfclab  34992  cnambfre  35104  triantru3  35659  lub0N  36484  glb0N  36488  cvlsupr3  36639  isdomn3  40145  ifpdfor2  40166  ifpdfor  40170  ifpim1  40174  ifpid2  40176  ifpim2  40177  ifpid2g  40198  ifpid1g  40199  ifpim23g  40200  ifpim1g  40206  ifpimimb  40209  rp-isfinite6  40223  rababg  40270  relnonrel  40284  dffrege115  40676  funressnfv  43632  dfnelbr2  43826
  Copyright terms: Public domain W3C validator