![]() |
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 318 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | 1 | imbi1i 353 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) |
3 | df-or 845 | . 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) | |
4 | 2, 3 | bitr4i 281 | 1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∨ wo 844 |
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 210 df-or 845 |
This theorem is referenced by: imori 851 imorri 852 pm4.62 853 pm4.78 932 pm4.52 982 dfifp4 1062 dfifp5 1063 dfifp7 1065 norasslem1 1531 rb-bijust 1751 rb-imdf 1752 rb-ax1 1754 nf2 1787 relsnb 5639 soxp 7806 modom 8703 dffin7-2 9809 algcvgblem 15911 divgcdodd 16044 chrelat2i 30148 disjex 30355 disjexc 30356 meran1 33872 meran3 33874 bj-dfbi5 34020 bj-andnotim 34035 itg2addnclem2 35109 dvasin 35141 impor 35519 biimpor 35522 hlrelat2 36699 ifpim1 40177 ifpim2 40180 ifpidg 40199 ifpim23g 40203 ifpim123g 40208 ifpimimb 40212 ifpororb 40213 sqrtcvallem1 40331 hbimpgVD 41610 stoweidlem14 42656 fvmptrabdm 43849 alimp-surprise 45308 eximp-surprise 45312 |
Copyright terms: Public domain | W3C validator |