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 486 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
3 | 1, 2 | nsyl 142 | 1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: bianfd 538 3bior1fand 1478 pr1eqbg 4767 iresn0n0 5923 fvmptopab 7266 wemappo 9165 axrepnd 10208 axunnd 10210 fzpreddisj 13161 sadadd2lem2 16009 smumullem 16051 nndvdslegcd 16064 divgcdnn 16074 sqgcd 16122 coprm 16268 isnmnd 18177 nfimdetndef 21486 mdetfval1 21487 ibladdlem 24717 lgsval2lem 26188 lgsval4a 26200 lgsdilem 26205 2sqcoprm 26316 addsqn2reurex2 26326 nbgrnself 27447 wwlks 27919 iswspthsnon 27940 clwwlknon1nloop 28182 clwwlknon1le1 28184 nfrgr2v 28355 hashxpe 30847 acycgr0v 32823 prclisacycgr 32826 fmlasucdisj 33074 frxp2 33528 frxp3 33534 nosepdmlem 33623 nodenselem8 33631 nosupbnd2lem1 33655 dfrdg4 33990 finxpreclem3 35301 finxpreclem5 35303 ibladdnclem 35570 dihatlat 39085 xppss12 39917 jm2.23 40521 ltnelicc 42710 limciccioolb 42837 dvmptfprodlem 43160 stoweidlem26 43242 fourierdlem12 43335 fourierdlem42 43365 divgcdoddALTV 44807 |
Copyright terms: Public domain | W3C validator |