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 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 |