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 213 | . 2 ⊢ (𝜓 ↔ 𝜑) |
4 | 1, 3 | mtbi 311 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 195 |
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 |
This theorem is referenced by: fal 1482 nemtbir 2877 ru 3401 pssirr 3669 indifdir 3842 noel 3878 npss0OLD 3967 iun0 4512 0iun 4513 br0 4631 vprc 4724 iin0 4765 nfnid 4823 opelopabsb 4910 0nelxp 5067 0nelxpOLD 5068 dm0 5260 cnv0 5454 co02 5566 nlim0 5700 snsn0non 5763 imadif 5887 0fv 6137 snnex 6862 iprc 6993 tfr2b 7379 tz7.44lem1 7388 tz7.48-3 7426 canth2 7998 pwcdadom 8921 canthp1lem2 9354 pwxpndom2 9366 adderpq 9657 mulerpq 9658 0ncn 9833 ax1ne0 9860 pnfnre 9960 mnfnre 9961 inelr 10887 xrltnr 11829 fzouzdisj 12373 lsw0 13205 fprodn0f 14561 eirr 14772 ruc 14811 aleph1re 14813 sqrt2irr 14817 sadc0 15014 1nprm 15230 3prm 15244 prmrec 15464 meet0 16960 join0 16961 odhash 17812 00lsp 18802 zringndrg 19657 zfbas 21510 ustn0 21834 zclmncvs 22756 lhop 23583 dvrelog 24183 axlowdimlem13 25634 uvtx01vtx 26020 avril1 26711 helloworld 26713 topnfbey 26717 vsfval 26872 dmadjrnb 28149 xrge00 29017 esumrnmpt2 29457 measvuni 29604 sibf0 29723 ballotlem4 29887 signswch 29964 bnj521 30059 3pm3.2ni 30849 elpotr 30930 dfon2lem7 30938 poseq 30994 nosgnn0 31055 sltsolem1 31067 linedegen 31420 mont 31578 subsym1 31596 limsucncmpi 31614 bj-ru1 32125 bj-0nel1 32133 bj-pinftynrr 32286 bj-minftynrr 32290 bj-pinftynminfty 32291 finxp0 32404 poimirlem30 32609 diophren 36395 eqneltri 38272 stoweidlem44 38937 fourierdlem62 39061 salexct2 39233 aisbnaxb 39727 dandysum2p2e4 39814 257prm 40011 fmtno4nprmfac193 40024 139prmALT 40049 31prm 40050 127prm 40053 nnsum4primeseven 40216 nnsum4primesevenALTV 40217 ntrl2v2e 41325 konigsberglem4 41425 0nodd 41600 2nodd 41602 1neven 41722 2zrngnring 41742 ex-gt 42268 alsi-no-surprise 42351 |
Copyright terms: Public domain | W3C validator |