| 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 | notbii 203 |
. 2
|
| 4 | 1, 3 | mpbir 206 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: nemtbir 1934 ru 2284 pssirr 2540 npss0 2735 iun0 3130 0iun 3132 vprc 3264 iin0 3292 opprc1b 3357 nlim0 3536 snsn0non 3599 snnex 3612 0nelxp 3877 dm0 3981 iprc 4021 co02 4222 imadif 4304 tz7.44lem1 4946 tz7.44-2 4948 tz7.48-3 4978 canth2 5359 undefnel2 5369 rankpw 5604 zorn 5755 brdom3 5759 cfsuc 5859 0npq 5998 1pr 6065 0nsr 6136 0ncn 6199 ax1ne0 6229 pnfnre 6461 mnfnre 6462 xrltnr 6512 nn0sub 7165 sqr2irr 7774 inelr 7780 climubii 8208 eirr 8451 ruclem35 8608 ruclem37 8610 ruc 8613 aleph1re 8615 tpsex 8669 vsfval 9381 avril1 9937 helloworld 9939 fsubbas 10073 zrdivrng 10210 dmadjrnb 11259 bnj521 12314 1nprm 13561 3prm 13572 3pm3.2ni 13602 indifdi 13617 elpotr 13638 dfon2lem7 13646 poseq 13746 sltval2 13789 nosgnn0 13791 axsltsolem1 13796 mont 13889 subsym1 13981 inpc 14343 zrfld 14507 top2usne 14618 elfiun 15051 ufilen 15261 compne 16099 |
| 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 163 |