![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con3dimp | Structured version Visualization version GIF version |
Description: Variant of con3d 150 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 150 | . 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
3 | 2 | imp 396 | 1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 385 |
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 199 df-an 386 |
This theorem is referenced by: stoic1a 1868 nelneq 2900 nelneq2 2901 nelss 3858 dtru 5038 sofld 5796 2f1fvneq 6743 card2inf 8700 gchen1 9733 gchen2 9734 bcpasc 13357 fiinfnf1o 13386 hashfn 13410 swrdnd2 13681 swrdccat 13796 swrdccatOLD 13797 nnoddn2prmb 15848 pcprod 15929 lubval 17296 glbval 17309 mplmonmul 19784 regr1lem 21868 blcld 22635 stdbdxmet 22645 itgss 23916 isosctrlem2 24898 isppw2 25190 dchrelbas3 25312 lgsdir 25406 2lgslem2 25469 2lgs 25481 rplogsum 25565 nb3grprlem2 26617 orngsqr 30312 qqhval2lem 30533 qqhf 30538 esumpinfval 30643 bj-dtru 33285 lindsenlbs 33885 poimirlem24 33914 isfldidl 34346 lssat 35029 paddasslem1 35833 lcfrlem21 37576 hdmap10lem 37852 hdmap11lem2 37855 jm2.23 38336 ntrneiel2 39154 ntrneik4w 39168 cncfiooicclem1 40838 fourierdlem81 41135 |
Copyright terms: Public domain | W3C validator |