![]() |
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 397 | 1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 386 |
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 387 |
This theorem is referenced by: stoic1a 1816 nelneq 2883 nelneq2 2884 nelss 3883 dtru 5082 sofld 5835 2f1fvneq 6789 card2inf 8749 gchen1 9782 gchen2 9783 bcpasc 13426 fiinfnf1o 13455 hashfn 13479 swrdnd2 13750 swrdccat 13865 swrdccatOLD 13866 nnoddn2prmb 15922 pcprod 16003 lubval 17370 glbval 17383 mplmonmul 19861 regr1lem 21951 blcld 22718 stdbdxmet 22728 itgss 24015 isosctrlem2 24997 isppw2 25293 dchrelbas3 25415 lgsdir 25509 2lgslem2 25572 2lgs 25584 rplogsum 25668 nb3grprlem2 26729 orngsqr 30366 qqhval2lem 30623 qqhf 30628 esumpinfval 30733 bj-dtru 33373 eldifsnneq 33732 lindsenlbs 34030 poimirlem24 34059 isfldidl 34491 lssat 35170 paddasslem1 35974 lcfrlem21 37717 hdmap10lem 37993 hdmap11lem2 37996 jm2.23 38522 ntrneiel2 39340 ntrneik4w 39354 cncfiooicclem1 41034 fourierdlem81 41331 |
Copyright terms: Public domain | W3C validator |