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 316 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | 1 | imbi1i 351 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) |
3 | df-or 842 | . 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) | |
4 | 2, 3 | bitr4i 279 | 1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∨ wo 841 |
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 208 df-or 842 |
This theorem is referenced by: imori 848 imorri 849 pm4.62 850 pm4.78 928 pm4.52 978 dfifp4 1058 dfifp5 1059 dfifp7 1061 norasslem1 1521 rb-bijust 1741 rb-imdf 1742 rb-ax1 1744 nf2 1777 r19.30OLD 3336 relsnb 5668 soxp 7812 modom 8707 dffin7-2 9808 algcvgblem 15909 divgcdodd 16042 chrelat2i 30069 disjex 30270 disjexc 30271 meran1 33656 meran3 33658 bj-dfbi5 33804 bj-andnotim 33819 itg2addnclem2 34825 dvasin 34859 impor 35240 biimpor 35243 hlrelat2 36419 ifpim1 39712 ifpim2 39715 ifpidg 39735 ifpim23g 39739 ifpim123g 39744 ifpimimb 39748 ifpororb 39749 hbimpgVD 41115 stoweidlem14 42176 fvmptrabdm 43369 alimp-surprise 44809 eximp-surprise 44813 |
Copyright terms: Public domain | W3C validator |