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  375  dftru2  1544  bitru  1548  vjust  3423  dfnul3OLD  4259  ab0orv  4309  pwv  4833  int0  4890  0iin  4989  domepOLD  5822  dfpo2  6188  orduninsuc  7665  fo1st  7824  fo2nd  7825  1st2val  7832  2nd2val  7833  eqer  8491  ener  8742  ruv  9291  acncc  10127  grothac  10517  grothtsk  10522  hashneq0  14007  rexfiuz  14987  sa-abvi  30706  signswch  32440  satfdm  33231  fobigcup  34129  elhf2  34404  limsucncmpi  34561  bj-vjust  35153  ruvALT  40096  uunT1  42289  nabctnabc  44313  clifte  44317  cliftet  44318  clifteta  44319  cliftetb  44320  confun5  44325  pldofph  44327  icht  44792  lco0  45656  line2ylem  45985
  Copyright terms: Public domain W3C validator