| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > con3dimp | Structured version Visualization version GIF version | ||
| Description: Variant of con3d 152 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| Ref | Expression |
|---|---|
| con3dimp.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| Ref | Expression |
|---|---|
| con3dimp | ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con3dimp.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | 1 | con3d 152 | . 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
| 3 | 2 | imp 406 | 1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 |
| 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-an 396 |
| This theorem is referenced by: stoic1a 1772 nelneq 2865 nelneq2 2866 nelss 4049 dtruALT2 5370 dtruOLD 5446 sofld 6207 2f1fvneq 7280 card2inf 9595 gchen1 10665 gchen2 10666 bcpasc 14360 fiinfnf1o 14389 hashfn 14414 swrdnd2 14693 swrdccat 14773 nnoddn2prmb 16851 pcprod 16933 lubval 18401 glbval 18414 mplmonmul 22054 regr1lem 23747 blcld 24518 stdbdxmet 24528 itgss 25847 isosctrlem2 26862 isppw2 27158 dchrelbas3 27282 lgsdir 27376 2lgslem2 27439 2lgs 27451 rplogsum 27571 nb3grprlem2 29398 orngsqr 33334 qqhval2lem 33982 qqhf 33987 esumpinfval 34074 spthcycl 35134 lindsenlbs 37622 poimirlem24 37651 isfldidl 38075 lssat 39017 paddasslem1 39822 lcfrlem21 41565 hdmap10lem 41841 hdmap11lem2 41844 fsuppssind 42603 jm2.23 43008 ntrneiel2 44099 ntrneik4w 44113 cncfiooicclem1 45908 fourierdlem81 46202 |
| Copyright terms: Public domain | W3C validator |