| 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 209 | 1 ⊢ (𝜑 ↔ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: monothetic 266 2false 375 dftru2 1545 bitru 1549 vjust 3481 ab0orv 4383 pwv 4904 int0 4962 0iin 5064 dfpo2 6316 orduninsuc 7864 fo1st 8034 fo2nd 8035 1st2val 8042 2nd2val 8043 eqer 8781 ener 9041 ruv 9642 acncc 10480 grothac 10870 grothtsk 10875 hashneq0 14403 rexfiuz 15386 sa-abvi 32462 signswch 34576 satfdm 35374 fobigcup 35901 elhf2 36176 limsucncmpi 36446 bj-vjust 37056 ruvALT 42679 oaordnrex 43308 omnord1ex 43317 oenord1ex 43328 uunT1 44800 nabctnabc 46943 clifte 46947 cliftet 46948 clifteta 46949 cliftetb 46950 confun5 46955 pldofph 46957 icht 47439 lco0 48344 line2ylem 48672 |
| Copyright terms: Public domain | W3C validator |