![]() |
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 410 | 1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 |
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-an 400 |
This theorem is referenced by: stoic1a 1774 nelneq 2914 nelneq2 2915 nelss 3978 dtru 5236 sofld 6011 2f1fvneq 6996 card2inf 9003 gchen1 10036 gchen2 10037 bcpasc 13677 fiinfnf1o 13706 hashfn 13732 swrdnd2 14008 swrdccat 14088 nnoddn2prmb 16140 pcprod 16221 lubval 17586 glbval 17599 mplmonmul 20704 regr1lem 22344 blcld 23112 stdbdxmet 23122 itgss 24415 isosctrlem2 25405 isppw2 25700 dchrelbas3 25822 lgsdir 25916 2lgslem2 25979 2lgs 25991 rplogsum 26111 nb3grprlem2 27171 orngsqr 30928 qqhval2lem 31332 qqhf 31337 esumpinfval 31442 spthcycl 32489 bj-dtru 34254 lindsenlbs 35052 poimirlem24 35081 isfldidl 35506 lssat 36312 paddasslem1 37116 lcfrlem21 38859 hdmap10lem 39135 hdmap11lem2 39138 fsuppssind 39459 jm2.23 39937 ntrneiel2 40789 ntrneik4w 40803 cncfiooicclem1 42535 fourierdlem81 42829 |
Copyright terms: Public domain | W3C validator |