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 199 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 |
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 197 |
This theorem is referenced by: 2false 365 trujust 1485 dftru2 1491 bitru 1496 vjust 3201 dfnul2 3917 dfnul3 3918 rab0OLD 3956 pwv 4433 int0 4490 int0OLD 4491 0iin 4578 snnexOLD 6967 orduninsuc 7043 fo1st 7188 fo2nd 7189 1st2val 7194 2nd2val 7195 eqer 7777 eqerOLD 7778 ener 8002 enerOLD 8003 ruv 8507 acncc 9262 grothac 9652 grothtsk 9657 hashneq0 13155 rexfiuz 14087 foo3 29302 signswch 30638 dfpo2 31645 domep 31698 fobigcup 32007 elhf2 32282 limsucncmpi 32444 bj-vjust 32786 bj-df-v 33016 uunT1 39007 nabctnabc 41098 clifte 41102 cliftet 41103 clifteta 41104 cliftetb 41105 confun5 41110 pldofph 41112 lco0 42216 |
Copyright terms: Public domain | W3C validator |