| 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 315 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
| 2 | 1 | imbi1i 349 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) |
| 3 | df-or 849 | . 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓)) | |
| 4 | 2, 3 | bitr4i 278 | 1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∨ wo 848 |
| 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 207 df-or 849 |
| This theorem is referenced by: imori 855 imorri 856 pm4.62 857 pm4.78 935 pm4.52 987 dfifp4 1067 dfifp5 1068 dfifp7 1070 norasslem1 1534 rb-bijust 1749 rb-imdf 1750 rb-ax1 1752 nf2 1785 relsnb 5812 soxp 8154 modom 9280 dffin7-2 10438 algcvgblem 16614 divgcdodd 16747 noinfprefixmo 27746 chrelat2i 32384 disjex 32605 disjexc 32606 meran1 36412 meran3 36414 bj-dfbi5 36575 bj-andnotim 36589 itg2addnclem2 37679 dvasin 37711 impor 38088 biimpor 38091 moeu2 38363 hlrelat2 39405 sticksstones1 42147 flt4lem7 42669 nna4b4nsq 42670 ifpim1 43482 ifpim2 43485 ifpidg 43504 ifpim23g 43508 ifpim123g 43513 ifpimimb 43517 ifpororb 43518 sqrtcvallem1 43644 hbimpgVD 44924 stoweidlem14 46029 fvmptrabdm 47305 fullthinc 49099 alimp-surprise 49299 eximp-surprise 49303 |
| Copyright terms: Public domain | W3C validator |