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

Theorem 2th 263
Description: Two truths are equivalent. (Contributed by NM, 18-Aug-1993.)
Hypotheses
Ref Expression
2th.1 𝜑
2th.2 𝜓
Assertion
Ref Expression
2th (𝜑𝜓)

Proof of Theorem 2th
StepHypRef Expression
1 2th.2 . . 3 𝜓
21a1i 11 . 2 (𝜑𝜓)
3 2th.1 . . 3 𝜑
43a1i 11 . 2 (𝜓𝜑)
52, 4impbii 208 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205
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
This theorem is referenced by:  monothetic  265  2false  374  dftru2  1538  bitru  1542  vjust  3462  dfnul3OLD  4328  ab0orv  4380  pwv  4906  int0  4966  0iin  5068  dfpo2  6302  orduninsuc  7848  fo1st  8014  fo2nd  8015  1st2val  8022  2nd2val  8023  eqer  8760  ener  9022  ruv  9627  acncc  10465  grothac  10855  grothtsk  10860  hashneq0  14359  rexfiuz  15330  sa-abvi  32325  signswch  34324  satfdm  35110  fobigcup  35627  elhf2  35902  limsucncmpi  36060  bj-vjust  36665  ruvALT  42228  oaordnrex  42866  omnord1ex  42875  oenord1ex  42886  uunT1  44361  nabctnabc  46451  clifte  46455  cliftet  46456  clifteta  46457  cliftetb  46458  confun5  46463  pldofph  46465  icht  46929  lco0  47681  line2ylem  48010
  Copyright terms: Public domain W3C validator