![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mtbir | Structured version Visualization version Unicode 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 207 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mtbi 304 |
1
![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 |
This theorem is referenced by: fal 1461 nonconneOLD 2647 nemtbir 2730 ru 3277 pssirr 3544 indifdir 3710 noel 3746 npss0 3814 iun0 4347 0iun 4348 br0 4462 vprc 4554 iin0 4590 nfnid 4642 opelopabsb 4724 0nelxp 4880 dm0 5066 co02 5367 nlim0 5499 snsn0non 5559 imadif 5679 0fv 5920 snnex 6623 iprc 6754 tfr2b 7139 tz7.44lem1 7148 tz7.48-3 7186 canth2 7750 pwcdadom 8671 canthp1lem2 9103 pwxpndom2 9115 adderpq 9406 mulerpq 9407 0ncn 9582 ax1ne0 9609 pnfnre 9707 mnfnre 9708 inelr 10626 xrltnr 11449 fzouzdisj 11984 lsw0 12747 fprodn0f 14093 eirr 14305 ruc 14343 aleph1re 14345 sqrt2irr 14349 sadc0 14476 1nprm 14677 3prm 14689 prmrec 14914 meet0 16431 join0 16432 odhash 17271 00lsp 18252 zfbas 20959 ustn0 21283 lhop 23016 dvrelog 23630 axlowdimlem13 25032 uvtx01vtx 25268 avril1 25948 helloworld 25950 topnfbey 25954 vsfval 26302 dmadjrnb 27607 xrge00 28496 esumrnmpt2 28937 measvuni 29084 sibf0 29215 ballotlem4 29379 signswch 29498 bnj521 29593 3pm3.2ni 30393 elpotr 30475 dfon2lem7 30483 poseq 30539 nosgnn0 30593 sltsolem1 30605 linedegen 30958 mont 31117 subsym1 31135 limsucncmpi 31153 bj-ru1 31582 bj-0nel1 31590 bj-pinftynrr 31708 bj-minftynrr 31712 bj-pinftynminfty 31713 finxp0 31827 poimirlem30 32014 diophren 35700 eqneltri 37458 stoweidlem44 37942 fourierdlem62 38069 salexct2 38235 aisbnaxb 38535 dandysum2p2e4 38623 nnsum4primeseven 38932 nnsum4primesevenALTV 38933 ntrl2v2e 39872 0nodd 40082 2nodd 40084 1neven 40204 2zrngnring 40224 ex-gt 40720 alsi-no-surprise 40807 |
Copyright terms: Public domain | W3C validator |