![]() |
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 322 | 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 1489 fal 1556 eqneltri 2857 nemtbir 3041 ru 3739 pssirr 4061 indifdirOLD 4246 noel 4291 noelOLD 4292 iun0 5023 0iun 5024 br0 5155 vprc 5273 iin0 5318 nfnid 5331 opelopabsb 5488 0nelopab 5525 0nelxp 5668 0xp 5731 nrelv 5757 dm0 5877 cnv0 6094 co02 6213 nlim0 6377 snsn0non 6443 imadif 6586 0fv 6887 poxp2 8076 poseq 8091 tz7.44lem1 8352 nlim1 8436 nlim2 8437 sdom0 9053 canth2 9075 snnen2o 9182 1sdom2 9185 canthp1lem2 10590 pwxpndom2 10602 adderpq 10893 mulerpq 10894 0ncn 11070 ax1ne0 11097 inelr 12144 xrltnr 13041 fzouzdisj 13609 lsw0 14454 eirr 16088 ruc 16126 aleph1re 16128 sqrt2irr 16132 n2dvds1 16251 n2dvds3 16254 sadc0 16335 1nprm 16556 join0 18295 meet0 18296 smndex1n0mnd 18723 nsmndex1 18724 smndex2dnrinv 18726 odhash 19357 cnfldfun 20811 zringndrg 20892 zfbas 23250 ustn0 23575 zclmncvs 24515 lhop 25383 dvrelog 25995 nosgnn0 27009 sltsolem1 27026 addsid1 27279 axlowdimlem13 27906 ntrl2v2e 29105 konigsberglem4 29202 avril1 29410 helloworld 29412 topnfbey 29416 vsfval 29578 dmadjrnb 30851 xrge00 31880 esumrnmpt2 32670 measvuni 32816 sibf0 32937 ballotlem4 33101 signswch 33176 satf0n0 33975 fmlaomn0 33987 gonan0 33989 goaln0 33990 fmla0disjsuc 33995 elpotr 34359 dfon2lem7 34367 muls01 34412 muls02 34413 mulsid1 34414 mulsid2 34415 linedegen 34731 nmotru 34883 limsucncmpi 34920 bj-ru1 35417 bj-0nel1 35427 bj-inftyexpitaudisj 35679 bj-pinftynminfty 35701 finxp0 35865 poimirlem30 36111 coss0 36944 epnsymrel 37027 diophren 41139 notbicom 43388 rexanuz2nf 43735 stoweidlem44 44292 fourierdlem62 44416 salexct2 44587 aisbnaxb 45153 dandysum2p2e4 45240 iota0ndef 45280 aiota0ndef 45336 257prm 45760 fmtno4nprmfac193 45773 139prmALT 45795 31prm 45796 127prm 45798 nnsum4primeseven 45999 nnsum4primesevenALTV 46000 0nodd 46111 2nodd 46113 1neven 46237 2zrngnring 46257 ex-gt 47180 alsi-no-surprise 47250 |
Copyright terms: Public domain | W3C validator |