Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > con3dimp | Structured version Visualization version GIF version |
Description: Variant of con3d 155 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 155 | . 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
3 | 2 | imp 409 | 1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: stoic1a 1773 nelneq 2937 nelneq2 2938 nelss 4030 eldifsnneqOLD 4724 dtru 5271 sofld 6044 2f1fvneq 7018 card2inf 9019 gchen1 10047 gchen2 10048 bcpasc 13682 fiinfnf1o 13711 hashfn 13737 swrdnd2 14017 swrdccat 14097 nnoddn2prmb 16150 pcprod 16231 lubval 17594 glbval 17607 mplmonmul 20245 regr1lem 22347 blcld 23115 stdbdxmet 23125 itgss 24412 isosctrlem2 25397 isppw2 25692 dchrelbas3 25814 lgsdir 25908 2lgslem2 25971 2lgs 25983 rplogsum 26103 nb3grprlem2 27163 orngsqr 30877 qqhval2lem 31222 qqhf 31227 esumpinfval 31332 spthcycl 32376 bj-dtru 34139 lindsenlbs 34902 poimirlem24 34931 isfldidl 35361 lssat 36167 paddasslem1 36971 lcfrlem21 38714 hdmap10lem 38990 hdmap11lem2 38993 jm2.23 39613 ntrneiel2 40456 ntrneik4w 40470 cncfiooicclem1 42196 fourierdlem81 42492 |
Copyright terms: Public domain | W3C validator |