| 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 482 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
| 3 | 1, 2 | nsyl 140 | 1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: bianfd 534 3bior1fand 1478 pr1eqbg 4857 iresn0n0 6072 fvmptopabOLD 7488 frxp2 8169 frxp3 8176 wemappo 9589 axrepnd 10634 axunnd 10636 fzpreddisj 13613 sadadd2lem2 16487 smumullem 16529 nndvdslegcd 16542 divgcdnn 16552 sqgcd 16599 coprm 16748 isnmnd 18751 nfimdetndef 22595 mdetfval1 22596 ibladdlem 25855 lgsval2lem 27351 lgsval4a 27363 lgsdilem 27368 2sqcoprm 27479 addsqn2reurex2 27489 nosepdmlem 27728 nodenselem8 27736 nosupbnd2lem1 27760 nbgrnself 29376 wwlks 29855 iswspthsnon 29876 clwwlknon1nloop 30118 clwwlknon1le1 30120 nfrgr2v 30291 hashxpe 32811 acycgr0v 35153 prclisacycgr 35156 fmlasucdisj 35404 dfrdg4 35952 finxpreclem3 37394 finxpreclem5 37396 ibladdnclem 37683 dihatlat 41336 xppss12 42268 jm2.23 43008 rexanuz2nf 45503 ltnelicc 45510 limciccioolb 45636 dvmptfprodlem 45959 stoweidlem26 46041 fourierdlem12 46134 fourierdlem42 46164 divgcdoddALTV 47669 |
| Copyright terms: Public domain | W3C validator |