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 375 dftru2 1544 bitru 1548 vjust 3423 dfnul3OLD 4259 ab0orv 4309 pwv 4833 int0 4890 0iin 4989 domepOLD 5822 dfpo2 6188 orduninsuc 7665 fo1st 7824 fo2nd 7825 1st2val 7832 2nd2val 7833 eqer 8491 ener 8742 ruv 9291 acncc 10127 grothac 10517 grothtsk 10522 hashneq0 14007 rexfiuz 14987 sa-abvi 30706 signswch 32440 satfdm 33231 fobigcup 34129 elhf2 34404 limsucncmpi 34561 bj-vjust 35153 ruvALT 40096 uunT1 42289 nabctnabc 44313 clifte 44317 cliftet 44318 clifteta 44319 cliftetb 44320 confun5 44325 pldofph 44327 icht 44792 lco0 45656 line2ylem 45985 |
Copyright terms: Public domain | W3C validator |