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 210 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 |
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 208 |
This theorem is referenced by: monothetic 267 2false 377 dftru2 1533 bitru 1537 vjust 3493 dfnul2OLD 4291 dfnul3 4292 pwv 4827 int0 4881 0iin 4978 domepOLD 5787 orduninsuc 7547 fo1st 7698 fo2nd 7699 1st2val 7706 2nd2val 7707 eqer 8313 ener 8544 ruv 9054 acncc 9850 grothac 10240 grothtsk 10245 hashneq0 13713 rexfiuz 14695 sa-abvi 30147 signswch 31730 satfdm 32513 dfpo2 32888 fobigcup 33258 elhf2 33533 limsucncmpi 33690 bj-df-v 34241 uunT1 40991 nabctnabc 43044 clifte 43048 cliftet 43049 clifteta 43050 cliftetb 43051 confun5 43056 pldofph 43058 lco0 44410 line2ylem 44666 |
Copyright terms: Public domain | W3C validator |