![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2th | Structured version Visualization version GIF version |
Description: Two truths are equivalent. (Contributed by NM, 18-Aug-1993.) |
Ref | Expression |
---|---|
2th.1 | ⊢ 𝜑 |
2th.2 | ⊢ 𝜓 |
Ref | Expression |
---|---|
2th | ⊢ (𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2th.2 | . . 3 ⊢ 𝜓 | |
2 | 1 | a1i 11 | . 2 ⊢ (𝜑 → 𝜓) |
3 | 2th.1 | . . 3 ⊢ 𝜑 | |
4 | 3 | a1i 11 | . 2 ⊢ (𝜓 → 𝜑) |
5 | 2, 4 | impbii 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 |