![]() |
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 214 | . 2 ⊢ (𝜓 ↔ 𝜑) |
4 | 1, 3 | mtbi 311 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 |
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 197 |
This theorem is referenced by: fal 1638 nemtbir 3038 ru 3586 pssirr 3857 indifdir 4032 noel 4067 iun0 4710 0iun 4711 br0 4835 vprc 4931 iin0 4970 nfnid 5025 opelopabsb 5118 0nelxp 5283 0nelxpOLD 5284 0xp 5339 nrelv 5383 dm0 5477 cnv0 5676 co02 5793 nlim0 5926 snsn0non 5989 imadif 6113 0fv 6368 snnexOLD 7114 iprc 7248 tfr2b 7645 tz7.44lem1 7654 tz7.48-3 7692 canth2 8269 pwcdadom 9240 canthp1lem2 9677 pwxpndom2 9689 adderpq 9980 mulerpq 9981 0ncn 10156 ax1ne0 10183 pnfnre 10283 mnfnre 10284 inelr 11212 xrltnr 12158 fzouzdisj 12712 lsw0 13549 fprodn0f 14928 eirr 15139 ruc 15178 aleph1re 15180 sqrt2irr 15185 sadc0 15384 1nprm 15599 3prm 15613 prmrec 15833 meet0 17345 join0 17346 odhash 18196 00lsp 19194 cnfldfunALT 19974 zringndrg 20053 zfbas 21920 ustn0 22244 zclmncvs 23167 lhop 23999 dvrelog 24604 axlowdimlem13 26055 ntrl2v2e 27338 konigsberglem4 27435 avril1 27661 helloworld 27663 topnfbey 27667 vsfval 27828 dmadjrnb 29105 xrge00 30026 esumrnmpt2 30470 measvuni 30617 sibf0 30736 ballotlem4 30900 signswch 30978 bnj521 31143 3pm3.2ni 31932 elpotr 32022 dfon2lem7 32030 poseq 32090 nosgnn0 32148 sltsolem1 32163 linedegen 32587 mont 32745 subsym1 32763 limsucncmpi 32781 bj-ru1 33265 bj-0nel1 33271 bj-pinftynrr 33446 bj-minftynrr 33450 bj-pinftynminfty 33451 finxp0 33565 poimirlem30 33772 coss0 34571 epnsymrel 34650 diophren 37903 eqneltri 39767 stoweidlem44 40778 fourierdlem62 40902 salexct2 41074 aisbnaxb 41598 dandysum2p2e4 41685 257prm 42001 fmtno4nprmfac193 42014 139prmALT 42039 31prm 42040 127prm 42043 nnsum4primeseven 42216 nnsum4primesevenALTV 42217 0nodd 42338 2nodd 42340 1neven 42460 2zrngnring 42480 ex-gt 43000 alsi-no-surprise 43073 |
Copyright terms: Public domain | W3C validator |