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 317 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | 1 | imbi1i 352 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) |
3 | df-or 844 | . 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) | |
4 | 2, 3 | bitr4i 280 | 1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∨ wo 843 |
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 209 df-or 844 |
This theorem is referenced by: imori 850 imorri 851 pm4.62 852 pm4.78 931 pm4.52 981 dfifp4 1061 dfifp5 1062 dfifp7 1064 norasslem1 1529 rb-bijust 1749 rb-imdf 1750 rb-ax1 1752 nf2 1785 r19.30OLD 3342 relsnb 5678 soxp 7826 modom 8722 dffin7-2 9823 algcvgblem 15924 divgcdodd 16057 chrelat2i 30145 disjex 30345 disjexc 30346 meran1 33763 meran3 33765 bj-dfbi5 33911 bj-andnotim 33926 itg2addnclem2 34948 dvasin 34982 impor 35363 biimpor 35366 hlrelat2 36543 ifpim1 39840 ifpim2 39843 ifpidg 39863 ifpim23g 39867 ifpim123g 39872 ifpimimb 39876 ifpororb 39877 hbimpgVD 41244 stoweidlem14 42306 fvmptrabdm 43499 alimp-surprise 44888 eximp-surprise 44892 |
Copyright terms: Public domain | W3C validator |