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 198 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 |
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 196 |
This theorem is referenced by: 2false 364 trujust 1477 dftru2 1483 bitru 1487 vjust 3174 dfnul2 3876 dfnul3 3877 rab0OLD 3910 pwv 4371 int0 4425 int0OLD 4426 0iin 4514 snnex 6862 orduninsuc 6935 fo1st 7079 fo2nd 7080 1st2val 7085 2nd2val 7086 eqer 7664 eqerOLD 7665 ener 7888 enerOLD 7889 ruv 8390 acncc 9145 grothac 9531 grothtsk 9536 hashneq0 13016 rexfiuz 13935 foo3 28686 signswch 29964 dfpo2 30898 domep 30942 fobigcup 31177 elhf2 31452 limsucncmpi 31614 bj-vjust 31974 bj-df-v 32207 uunT1 38028 nabctnabc 39747 clifte 39751 cliftet 39752 clifteta 39753 cliftetb 39754 confun5 39759 pldofph 39761 lco0 42010 |
Copyright terms: Public domain | W3C validator |