![]() |
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 307 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | 1 | imbi1i 341 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) |
3 | df-or 837 | . 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) | |
4 | 2, 3 | bitr4i 270 | 1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∨ wo 836 |
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 199 df-or 837 |
This theorem is referenced by: imori 843 imorri 844 pm4.62 845 pm4.78 921 pm4.52 970 dfifp4 1050 dfifp5 1051 dfifp7 1053 rb-bijust 1793 rb-imdf 1794 rb-ax1 1796 nf2 1829 r19.30 3268 relsnb 5475 soxp 7573 modom 8451 dffin7-2 9557 algcvgblem 15700 divgcdodd 15830 chrelat2i 29800 disjex 29972 disjexc 29973 meran1 32997 meran3 32999 bj-dfbi5 33141 bj-andnotim 33156 itg2addnclem2 34092 dvasin 34126 impor 34509 biimpor 34512 hlrelat2 35562 ifpim1 38781 ifpim2 38784 ifpidg 38804 ifpim23g 38808 ifpim123g 38813 ifpimimb 38817 ifpororb 38818 hbimpgVD 40083 stoweidlem14 41168 fvmptrabdm 42344 alimp-surprise 43642 eximp-surprise 43646 |
Copyright terms: Public domain | W3C validator |