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 472 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
3 | 1, 2 | nsyl 134 | 1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: bianfd 963 3bior1fand 1431 wemappo 8337 axrepnd 9295 axunnd 9297 fzpreddisj 12260 sadadd2lem2 15010 smumullem 15052 nndvdslegcd 15065 divgcdnn 15074 sqgcd 15116 divgcdodd 15260 coprm 15261 pythagtriplem19 15376 isnmnd 17121 nfimdetndef 20214 mdetfval1 20215 ibladdlem 23392 lgsval2lem 24832 lgsval4a 24844 lgsdilem 24849 uvtx01vtx 26020 clwlknclwlkdifs 26487 frgra2v 26526 2sqcoprm 28978 nodenselem8 31087 dfrdg4 31228 finxpreclem3 32406 finxpreclem5 32408 ibladdnclem 32636 dihatlat 35641 jm2.23 36581 ltnelicc 38566 limciccioolb 38688 dvmptfprodlem 38834 stoweidlem26 38919 fourierdlem12 39012 fourierdlem42 39042 divgcdoddALTV 40131 pr1eqbg 40313 nbgrnself 40583 wwlks 41038 clwwlknclwwlkdifs 41181 nfrgr2v 41442 |
Copyright terms: Public domain | W3C validator |