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 225 | . 2 ⊢ (𝜓 ↔ 𝜑) |
4 | 1, 3 | mtbi 323 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 |
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 208 |
This theorem is referenced by: fal 1542 eqneltri 2903 nemtbir 3109 ru 3768 pssirr 4074 indifdir 4257 noel 4293 noelOLD 4294 iun0 4976 0iun 4977 br0 5106 vprc 5210 iin0 5252 nfnid 5267 opelopabsb 5408 0nelxp 5582 0xp 5642 nrelv 5666 dm0 5783 cnv0 5992 co02 6106 nlim0 6242 snsn0non 6302 imadif 6431 0fv 6702 tz7.44lem1 8030 canth2 8658 canthp1lem2 10063 pwxpndom2 10075 adderpq 10366 mulerpq 10367 0ncn 10543 ax1ne0 10570 inelr 11616 xrltnr 12502 fzouzdisj 13061 lsw0 13905 eirr 15546 ruc 15584 aleph1re 15586 sqrt2irr 15590 n2dvds1 15705 n2dvds3 15709 sadc0 15791 1nprm 16011 meet0 17735 join0 17736 odhash 18628 cnfldfunALT 20486 zringndrg 20565 zfbas 22432 ustn0 22756 zclmncvs 23679 lhop 24540 dvrelog 25147 axlowdimlem13 26667 ntrl2v2e 27864 konigsberglem4 27961 avril1 28169 helloworld 28171 topnfbey 28175 vsfval 28337 dmadjrnb 29610 xrge00 30600 esumrnmpt2 31226 measvuni 31372 sibf0 31491 ballotlem4 31655 signswch 31730 bnj521 31906 satf0n0 32522 fmlaomn0 32534 gonan0 32536 goaln0 32537 fmla0disjsuc 32542 3pm3.2ni 32840 elpotr 32923 dfon2lem7 32931 poseq 32992 nosgnn0 33062 sltsolem1 33077 linedegen 33501 nmotru 33653 subsym1 33672 limsucncmpi 33690 bj-ru1 34151 bj-0nel1 34162 bj-inftyexpitaudisj 34379 bj-pinftynminfty 34401 bj-isrvec 34463 finxp0 34554 poimirlem30 34803 coss0 35599 epnsymrel 35678 diophren 39288 stoweidlem44 42206 fourierdlem62 42330 salexct2 42499 aisbnaxb 43024 dandysum2p2e4 43111 iota0ndef 43151 aiota0ndef 43172 257prm 43600 fmtno4nprmfac193 43613 139prmALT 43636 31prm 43637 127prm 43640 nnsum4primeseven 43842 nnsum4primesevenALTV 43843 0nodd 43954 2nodd 43956 smndex1n0mnd 44012 nsmndex1 44013 smndex2dnrinv 44015 1neven 44131 2zrngnring 44151 ex-gt 44755 alsi-no-surprise 44825 |
Copyright terms: Public domain | W3C validator |