![]() |
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 2853 nemtbir 3039 ru 3775 pssirr 4099 indifdirOLD 4284 noel 4329 noelOLD 4330 iun0 5064 0iun 5065 br0 5196 vprc 5314 iin0 5359 nfnid 5372 opelopabsb 5529 0nelopab 5566 0nelxp 5709 0xp 5772 nrelv 5798 dm0 5918 cnv0 6137 co02 6256 nlim0 6420 snsn0non 6486 imadif 6629 0fv 6932 poxp2 8124 poseq 8139 tz7.44lem1 8400 nlim1 8484 nlim2 8485 sdom0 9104 canth2 9126 snnen2o 9233 1sdom2 9236 canthp1lem2 10644 pwxpndom2 10656 adderpq 10947 mulerpq 10948 0ncn 11124 ax1ne0 11151 inelr 12198 xrltnr 13095 fzouzdisj 13664 lsw0 14511 eirr 16144 ruc 16182 aleph1re 16184 sqrt2irr 16188 n2dvds1 16307 n2dvds3 16310 sadc0 16391 1nprm 16612 join0 18354 meet0 18355 smndex1n0mnd 18789 nsmndex1 18790 smndex2dnrinv 18792 odhash 19435 cnfldfun 20941 zringndrg 21022 zfbas 23382 ustn0 23707 zclmncvs 24647 lhop 25515 dvrelog 26127 nosgnn0 27141 sltsolem1 27158 addsrid 27428 muls01 27548 mulsrid 27549 axlowdimlem13 28192 ntrl2v2e 29391 konigsberglem4 29488 avril1 29696 helloworld 29698 topnfbey 29702 vsfval 29864 dmadjrnb 31137 xrge00 32165 esumrnmpt2 33004 measvuni 33150 sibf0 33271 ballotlem4 33435 signswch 33510 satf0n0 34307 fmlaomn0 34319 gonan0 34321 goaln0 34322 fmla0disjsuc 34327 elpotr 34691 dfon2lem7 34699 linedegen 35053 nmotru 35231 limsucncmpi 35268 bj-ru1 35762 bj-0nel1 35772 bj-inftyexpitaudisj 36024 bj-pinftynminfty 36046 finxp0 36210 poimirlem30 36456 coss0 37287 epnsymrel 37370 diophren 41484 notbicom 43793 rexanuz2nf 44138 stoweidlem44 44695 fourierdlem62 44819 salexct2 44990 aisbnaxb 45556 dandysum2p2e4 45643 iota0ndef 45684 aiota0ndef 45740 257prm 46164 fmtno4nprmfac193 46177 139prmALT 46199 31prm 46200 127prm 46202 nnsum4primeseven 46403 nnsum4primesevenALTV 46404 0nodd 46515 2nodd 46517 1neven 46732 2zrngnring 46752 ex-gt 47675 alsi-no-surprise 47745 |
Copyright terms: Public domain | W3C validator |