| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: An inference from a biconditional, related to modus tollens. |
| Ref | Expression |
|---|---|
| mtbir.1 |
|
| mtbir.2 |
|
| Ref | Expression |
|---|---|
| mtbir |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mtbir.1 |
. 2
| |
| 2 | mtbir.2 |
. . 3
| |
| 3 | 2 | negbii 187 |
. 2
|
| 4 | 1, 3 | mpbir 190 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: nemtbir 1641 ru 1938 pssirr 2146 nvelv 2713 iin0 2740 opprc1b 2796 0nelxp 3240 dmsn0 3324 dmsnsn0 3325 inelv 3362 co02 3508 imadif 3574 tz7.44lem1 3927 tz7.44-2 3929 tz7.48-3 3958 canth2 4484 rankpw 4684 zorn 4797 brdom3 4801 cfsuc 4915 0npq 5050 1pr 5117 0nsr 5188 0ncn 5251 ax1ne0 5280 pnfnre 5496 mnfnre 5497 xrltnrt 5541 nn0subt 6161 sqr2irr 6729 inelr 6735 climubi 7153 eirr 7394 ruclem35 7544 ruclem37 7546 ruc 7549 aleph1re 7551 tpsex 7605 0vfval 8225 vsfval 8254 avril1 8784 helloworld 8786 dmadjrnb 9830 top2usne 10549 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 |
| This theorem depends on definitions: df-bi 147 |