![]() |
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 201 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 |
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 199 |
This theorem is referenced by: monothetic 258 2false 367 trujustOLD 1661 dftru2 1664 bitru 1668 vjust 3415 dfnul2 4146 dfnul3 4147 pwv 4655 int0 4711 0iin 4798 orduninsuc 7304 fo1st 7448 fo2nd 7449 1st2val 7456 2nd2val 7457 eqer 8044 ener 8269 ruv 8776 acncc 9577 grothac 9967 grothtsk 9972 hashneq0 13445 rexfiuz 14464 sa-abvi 29857 signswch 31185 dfpo2 32187 domep 32236 fobigcup 32546 elhf2 32821 limsucncmpi 32977 bj-vjust 33311 bj-df-v 33538 uunT1 39834 nabctnabc 41892 clifte 41896 cliftet 41897 clifteta 41898 cliftetb 41899 confun5 41904 pldofph 41906 lco0 43063 line2ylem 43303 |
Copyright terms: Public domain | W3C validator |