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

Theorem 2th 256
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 201 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 198
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 199
This theorem is referenced by:  monothetic  258  2false  367  trujustOLD  1661  dftru2  1664  bitru  1668  vjust  3415  dfnul2  4146  dfnul3  4147  pwv  4655  int0  4711  0iin  4798  orduninsuc  7304  fo1st  7448  fo2nd  7449  1st2val  7456  2nd2val  7457  eqer  8044  ener  8269  ruv  8776  acncc  9577  grothac  9967  grothtsk  9972  hashneq0  13445  rexfiuz  14464  sa-abvi  29857  signswch  31185  dfpo2  32187  domep  32236  fobigcup  32546  elhf2  32821  limsucncmpi  32977  bj-vjust  33311  bj-df-v  33538  uunT1  39834  nabctnabc  41892  clifte  41896  cliftet  41897  clifteta  41898  cliftetb  41899  confun5  41904  pldofph  41906  lco0  43063  line2ylem  43303
  Copyright terms: Public domain W3C validator