| 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 224 | . 2 ⊢ (𝜓 ↔ 𝜑) |
| 4 | 1, 3 | mtbi 322 | 1 ⊢ ¬ 𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 |
| 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 |
| This theorem is referenced by: 3pm3.2ni 1490 fal 1554 eqneltri 2860 nemtbir 3038 ru 3786 ruOLD 3787 pssirr 4103 noel 4338 iun0 5062 0iun 5063 br0 5192 vprc 5315 iin0 5362 nfnid 5375 opelopabsb 5535 0nelopab 5572 0nelxp 5719 0xp 5784 nrelv 5810 dm0 5931 cnv0 6160 co02 6280 nlim0 6443 snsn0non 6509 imadif 6650 0fv 6950 poxp2 8168 poseq 8183 tz7.44lem1 8445 nlim1 8527 nlim2 8528 sdom0 9148 canth2 9170 snnen2o 9273 1sdom2 9276 canthp1lem2 10693 pwxpndom2 10705 adderpq 10996 mulerpq 10997 0ncn 11173 ax1ne0 11200 inelr 12256 xrltnr 13161 fzouzdisj 13735 lsw0 14603 eirr 16241 ruc 16279 aleph1re 16281 sqrt2irr 16285 n2dvds1 16405 n2dvds3 16408 sadc0 16491 1nprm 16716 join0 18450 meet0 18451 smndex1n0mnd 18925 nsmndex1 18926 smndex2dnrinv 18928 odhash 19592 cnfldfun 21378 cnfldfunOLD 21391 zringndrg 21479 zfbas 23904 ustn0 24229 zclmncvs 25182 lhop 26055 dvrelog 26679 nosgnn0 27703 sltsolem1 27720 addsrid 27997 muls01 28138 mulsrid 28139 axlowdimlem13 28969 ntrl2v2e 30177 konigsberglem4 30274 avril1 30482 helloworld 30484 topnfbey 30488 vsfval 30652 dmadjrnb 31925 xrge00 33017 esumrnmpt2 34069 measvuni 34215 sibf0 34336 ballotlem4 34501 signswch 34576 satf0n0 35383 fmlaomn0 35395 gonan0 35397 goaln0 35398 fmla0disjsuc 35403 elpotr 35782 dfon2lem7 35790 linedegen 36144 nmotru 36409 limsucncmpi 36446 bj-ru1 36944 bj-0nel1 36954 bj-inftyexpitaudisj 37206 bj-pinftynminfty 37228 finxp0 37392 poimirlem30 37657 coss0 38480 epnsymrel 38563 diophren 42824 notbicom 45170 rexanuz2nf 45503 stoweidlem44 46059 fourierdlem62 46183 salexct2 46354 aisbnaxb 46923 dandysum2p2e4 47010 iota0ndef 47051 aiota0ndef 47109 257prm 47548 fmtno4nprmfac193 47561 139prmALT 47583 31prm 47584 127prm 47586 nnsum4primeseven 47787 nnsum4primesevenALTV 47788 usgrexmpl2trifr 47996 0nodd 48086 2nodd 48088 1neven 48154 2zrngnring 48174 ex-gt 49247 alsi-no-surprise 49315 |
| Copyright terms: Public domain | W3C validator |