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 1467 pr1eqbg 4779 iresn0n0 5916 fvmptopab 7198 wemappo 9001 axrepnd 10004 axunnd 10006 fzpreddisj 12944 sadadd2lem2 15787 smumullem 15829 nndvdslegcd 15842 divgcdnn 15851 sqgcd 15897 coprm 16043 isnmnd 17903 nfimdetndef 21126 mdetfval1 21127 ibladdlem 24347 lgsval2lem 25810 lgsval4a 25822 lgsdilem 25827 2sqcoprm 25938 addsqn2reurex2 25948 nbgrnself 27068 wwlks 27540 iswspthsnon 27561 clwwlknon1nloop 27805 clwwlknon1le1 27807 nfrgr2v 27978 hashxpe 30455 acycgr0v 32292 prclisacycgr 32295 fmlasucdisj 32543 nosepdmlem 33084 nodenselem8 33092 nosupbnd2lem1 33112 dfrdg4 33309 finxpreclem3 34556 finxpreclem5 34558 ibladdnclem 34829 dihatlat 38350 xppss12 38993 jm2.23 39471 ltnelicc 41648 limciccioolb 41778 dvmptfprodlem 42105 stoweidlem26 42188 fourierdlem12 42281 fourierdlem42 42311 divgcdoddALTV 43724 |
Copyright terms: Public domain | W3C validator |