![]() |
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 223 | . 2 ⊢ (𝜓 ↔ 𝜑) |
4 | 1, 3 | mtbi 321 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 |
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 |
This theorem is referenced by: 3pm3.2ni 1484 fal 1548 eqneltri 2845 nemtbir 3028 ru 3774 ruOLD 3775 pssirr 4099 indifdirOLD 4287 noel 4333 noelOLD 4334 iun0 5070 0iun 5071 br0 5202 vprc 5320 iin0 5366 nfnid 5379 opelopabsb 5536 0nelopab 5573 0nelxp 5716 0xp 5780 nrelv 5806 dm0 5927 cnv0 6152 co02 6271 nlim0 6435 snsn0non 6501 imadif 6643 0fv 6945 poxp2 8157 poseq 8172 tz7.44lem1 8435 nlim1 8519 nlim2 8520 sdom0 9146 canth2 9168 snnen2o 9271 1sdom2 9274 canthp1lem2 10696 pwxpndom2 10708 adderpq 10999 mulerpq 11000 0ncn 11176 ax1ne0 11203 inelr 12254 xrltnr 13153 fzouzdisj 13722 lsw0 14573 eirr 16207 ruc 16245 aleph1re 16247 sqrt2irr 16251 n2dvds1 16370 n2dvds3 16373 sadc0 16454 1nprm 16680 join0 18430 meet0 18431 smndex1n0mnd 18902 nsmndex1 18903 smndex2dnrinv 18905 odhash 19572 cnfldfun 21357 cnfldfunOLD 21370 zringndrg 21458 zfbas 23891 ustn0 24216 zclmncvs 25167 lhop 26040 dvrelog 26664 nosgnn0 27688 sltsolem1 27705 addsrid 27978 muls01 28113 mulsrid 28114 axlowdimlem13 28888 ntrl2v2e 30091 konigsberglem4 30188 avril1 30396 helloworld 30398 topnfbey 30402 vsfval 30566 dmadjrnb 31839 xrge00 32895 esumrnmpt2 33901 measvuni 34047 sibf0 34168 ballotlem4 34332 signswch 34407 satf0n0 35206 fmlaomn0 35218 gonan0 35220 goaln0 35221 fmla0disjsuc 35226 elpotr 35605 dfon2lem7 35613 linedegen 35967 nmotru 36120 limsucncmpi 36157 bj-ru1 36650 bj-0nel1 36660 bj-inftyexpitaudisj 36912 bj-pinftynminfty 36934 finxp0 37098 poimirlem30 37351 coss0 38177 epnsymrel 38260 diophren 42470 notbicom 44771 rexanuz2nf 45108 stoweidlem44 45665 fourierdlem62 45789 salexct2 45960 aisbnaxb 46526 dandysum2p2e4 46613 iota0ndef 46654 aiota0ndef 46710 257prm 47133 fmtno4nprmfac193 47146 139prmALT 47168 31prm 47169 127prm 47171 nnsum4primeseven 47372 nnsum4primesevenALTV 47373 0nodd 47547 2nodd 47549 1neven 47615 2zrngnring 47635 ex-gt 48474 alsi-no-surprise 48544 |
Copyright terms: Public domain | W3C validator |