![]() |
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 468 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
3 | 1, 2 | nsyl 137 | 1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 382 |
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 197 df-an 383 |
This theorem is referenced by: bianfd 1003 3bior1fand 1587 pr1eqbg 4522 fvmptopab 6845 wemappo 8611 axrepnd 9619 axunnd 9621 fzpreddisj 12598 sadadd2lem2 15381 smumullem 15423 nndvdslegcd 15436 divgcdnn 15445 sqgcd 15487 coprm 15631 pythagtriplem19 15746 isnmnd 17507 nfimdetndef 20614 mdetfval1 20615 ibladdlem 23807 lgsval2lem 25254 lgsval4a 25266 lgsdilem 25271 nbgrnself 26479 wwlks 26964 iswspthsnon 26987 clwwlknclwwlkdifsOLD 27130 clwwlknon1nloop 27275 clwwlknon1le1 27277 nfrgr2v 27455 2sqcoprm 29988 nosepdmlem 32171 nodenselem8 32179 nosupbnd2lem1 32199 dfrdg4 32396 finxpreclem3 33568 finxpreclem5 33570 ibladdnclem 33799 dihatlat 37145 xppss12 37778 jm2.23 38090 ltnelicc 40241 limciccioolb 40372 dvmptfprodlem 40678 stoweidlem26 40761 fourierdlem12 40854 fourierdlem42 40884 divgcdoddALTV 42122 |
Copyright terms: Public domain | W3C validator |