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

Theorem 2th 267
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 212 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 209
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
This theorem is referenced by:  monothetic  269  2false  379  dftru2  1548  bitru  1552  vjust  3422  dfnul3OLD  4258  ab0orv  4308  pwv  4831  int0  4888  0iin  4987  domepOLD  5808  dfpo2  6174  orduninsuc  7641  fo1st  7800  fo2nd  7801  1st2val  7808  2nd2val  7809  eqer  8447  ener  8698  ruv  9243  acncc  10079  grothac  10469  grothtsk  10474  hashneq0  13956  rexfiuz  14936  sa-abvi  30548  signswch  32276  satfdm  33067  fobigcup  33965  elhf2  34240  limsucncmpi  34397  bj-vjust  34989  ruvALT  39920  uunT1  42102  nabctnabc  44127  clifte  44131  cliftet  44132  clifteta  44133  cliftetb  44134  confun5  44139  pldofph  44141  icht  44606  lco0  45470  line2ylem  45799
  Copyright terms: Public domain W3C validator