![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > intnanrd | Structured version Visualization version GIF version |
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
Ref | Expression |
---|---|
intnand.1 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
intnanrd | ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | intnand.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
2 | simpl 483 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
3 | 1, 2 | nsyl 142 | 1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: bianfd 535 3bior1fand 1468 pr1eqbg 4700 fvmptopab 7075 wemappo 8866 axrepnd 9869 axunnd 9871 fzpreddisj 12810 sadadd2lem2 15636 smumullem 15678 nndvdslegcd 15691 divgcdnn 15700 sqgcd 15742 coprm 15888 isnmnd 17741 nfimdetndef 20886 mdetfval1 20887 ibladdlem 24107 lgsval2lem 25569 lgsval4a 25581 lgsdilem 25586 2sqcoprm 25697 addsqn2reurex2 25707 nbgrnself 26828 wwlks 27299 iswspthsnon 27320 clwwlknon1nloop 27564 clwwlknon1le1 27566 nfrgr2v 27739 hashxpe 30209 acycgr0v 32005 prclisacycgr 32008 fmlasucdisj 32256 nosepdmlem 32798 nodenselem8 32806 nosupbnd2lem1 32826 dfrdg4 33023 finxpreclem3 34226 finxpreclem5 34228 ibladdnclem 34500 dihatlat 38022 xppss12 38666 jm2.23 39099 ltnelicc 41335 limciccioolb 41465 dvmptfprodlem 41792 stoweidlem26 41875 fourierdlem12 41968 fourierdlem42 41998 divgcdoddALTV 43351 |
Copyright terms: Public domain | W3C validator |