![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mtbir | Structured version Visualization version GIF version |
Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.) |
Ref | Expression |
---|---|
mtbir.1 | ⊢ ¬ 𝜓 |
mtbir.2 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
mtbir | ⊢ ¬ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbir.1 | . 2 ⊢ ¬ 𝜓 | |
2 | mtbir.2 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | bicomi 216 | . 2 ⊢ (𝜓 ↔ 𝜑) |
4 | 1, 3 | mtbi 314 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 |
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 199 |
This theorem is referenced by: fal 1521 eqneltri 2860 nemtbir 3064 ru 3681 pssirr 3968 indifdir 4148 noel 4184 noelOLD 4185 iun0 4851 0iun 4852 br0 4978 vprc 5076 iin0 5115 nfnid 5129 opelopabsb 5271 0nelxp 5441 0xp 5499 nrelv 5523 dm0 5637 cnv0 5839 co02 5952 nlim0 6087 snsn0non 6147 imadif 6271 0fv 6539 tz7.44lem1 7845 canth2 8466 canthp1lem2 9873 pwxpndom2 9885 adderpq 10176 mulerpq 10177 0ncn 10353 ax1ne0 10380 inelr 11429 xrltnr 12331 fzouzdisj 12888 lsw0 13728 eirr 15418 ruc 15456 aleph1re 15458 sqrt2irr 15462 n2dvds1 15577 n2dvds3 15581 sadc0 15663 1nprm 15879 meet0 17605 join0 17606 odhash 18460 cnfldfunALT 20260 zringndrg 20339 zfbas 22208 ustn0 22532 zclmncvs 23455 lhop 24316 dvrelog 24921 axlowdimlem13 26443 ntrl2v2e 27687 konigsberglem4 27787 avril1 28019 helloworld 28021 topnfbey 28025 vsfval 28187 dmadjrnb 29464 xrge00 30402 esumrnmpt2 30968 measvuni 31115 sibf0 31234 ballotlem4 31399 signswch 31474 bnj521 31652 satf0n0 32185 3pm3.2ni 32460 elpotr 32543 dfon2lem7 32551 poseq 32613 nosgnn0 32683 sltsolem1 32698 linedegen 33122 nmotru 33274 subsym1 33292 limsucncmpi 33310 bj-ru1 33746 bj-0nel1 33758 bj-inftyexpitaudisj 33953 bj-pinftynminfty 33975 finxp0 34110 poimirlem30 34360 coss0 35161 epnsymrel 35240 diophren 38803 stoweidlem44 41758 fourierdlem62 41882 salexct2 42051 aisbnaxb 42575 dandysum2p2e4 42662 iota0ndef 42677 aiota0ndef 42699 257prm 43089 fmtno4nprmfac193 43102 139prmALT 43125 31prm 43126 127prm 43129 nnsum4primeseven 43331 nnsum4primesevenALTV 43332 0nodd 43443 2nodd 43445 1neven 43565 2zrngnring 43585 ex-gt 44192 alsi-no-surprise 44262 |
Copyright terms: Public domain | W3C validator |