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 847 | . 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) | |
4 | 2, 3 | bitr4i 281 | 1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∨ 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 210 df-or 847 |
This theorem is referenced by: imori 853 imorri 854 pm4.62 855 pm4.78 934 pm4.52 984 dfifp4 1066 dfifp5 1067 dfifp7 1069 norasslem1 1535 rb-bijust 1756 rb-imdf 1757 rb-ax1 1759 nf2 1792 relsnb 5640 soxp 7842 modom 8791 dffin7-2 9891 algcvgblem 16011 divgcdodd 16144 chrelat2i 30292 disjex 30497 disjexc 30498 noinfprefixmo 33537 meran1 34230 meran3 34232 bj-dfbi5 34382 bj-andnotim 34397 itg2addnclem2 35441 dvasin 35473 impor 35851 biimpor 35854 hlrelat2 37029 sticksstones1 39697 flt4lem7 40052 nna4b4nsq 40053 ifpim1 40614 ifpim2 40617 ifpidg 40636 ifpim23g 40640 ifpim123g 40645 ifpimimb 40649 ifpororb 40650 sqrtcvallem1 40768 hbimpgVD 42046 stoweidlem14 43081 fvmptrabdm 44302 alimp-surprise 45921 eximp-surprise 45925 |
Copyright terms: Public domain | W3C validator |