![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imor | Structured version Visualization version GIF version |
Description: Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) |
Ref | Expression |
---|---|
imor | ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotb 315 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | 1 | imbi1i 349 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) |
3 | df-or 847 | . 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) | |
4 | 2, 3 | bitr4i 278 | 1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∨ wo 846 |
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 df-or 847 |
This theorem is referenced by: imori 853 imorri 854 pm4.62 855 pm4.78 933 pm4.52 983 dfifp4 1065 dfifp5 1066 dfifp7 1068 norasslem1 1528 rb-bijust 1744 rb-imdf 1745 rb-ax1 1747 nf2 1780 relsnb 5798 soxp 8128 modom 9262 dffin7-2 10415 algcvgblem 16541 divgcdodd 16674 noinfprefixmo 27627 chrelat2i 32168 disjex 32375 disjexc 32376 meran1 35885 meran3 35887 bj-dfbi5 36040 bj-andnotim 36055 itg2addnclem2 37134 dvasin 37166 impor 37543 biimpor 37546 moeu2 37823 hlrelat2 38865 sticksstones1 41602 flt4lem7 42055 nna4b4nsq 42056 ifpim1 42871 ifpim2 42874 ifpidg 42893 ifpim23g 42897 ifpim123g 42902 ifpimimb 42906 ifpororb 42907 sqrtcvallem1 43033 hbimpgVD 44315 stoweidlem14 45374 fvmptrabdm 46645 fullthinc 48024 alimp-surprise 48185 eximp-surprise 48189 |
Copyright terms: Public domain | W3C validator |