![]() |
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 484 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
3 | 1, 2 | nsyl 140 | 1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: bianfd 536 3bior1fand 1477 pr1eqbg 4819 iresn0n0 6012 fvmptopabOLD 7417 frxp2 8081 frxp3 8088 wemappo 9492 axrepnd 10537 axunnd 10539 fzpreddisj 13497 sadadd2lem2 16337 smumullem 16379 nndvdslegcd 16392 divgcdnn 16402 sqgcd 16448 coprm 16594 isnmnd 18567 nfimdetndef 21954 mdetfval1 21955 ibladdlem 25200 lgsval2lem 26671 lgsval4a 26683 lgsdilem 26688 2sqcoprm 26799 addsqn2reurex2 26809 nosepdmlem 27047 nodenselem8 27055 nosupbnd2lem1 27079 nbgrnself 28349 wwlks 28822 iswspthsnon 28843 clwwlknon1nloop 29085 clwwlknon1le1 29087 nfrgr2v 29258 hashxpe 31751 acycgr0v 33782 prclisacycgr 33785 fmlasucdisj 34033 dfrdg4 34565 finxpreclem3 35893 finxpreclem5 35895 ibladdnclem 36163 dihatlat 39826 xppss12 40681 jm2.23 41349 rexanuz2nf 43802 ltnelicc 43809 limciccioolb 43936 dvmptfprodlem 44259 stoweidlem26 44341 fourierdlem12 44434 fourierdlem42 44464 divgcdoddALTV 45948 |
Copyright terms: Public domain | W3C validator |