![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbiri | Unicode version |
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
Ref | Expression |
---|---|
mpbiri.min |
![]() ![]() |
mpbiri.maj |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpbiri |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbiri.min |
. . 3
![]() ![]() | |
2 | 1 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | mpbiri.maj |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpbird 166 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.18im 1322 dedhb 2787 sbceqal 2897 ssdifeq0 3371 pwidg 3449 elpr2 3474 snidg 3479 exsnrex 3491 rabrsndc 3516 prid1g 3552 tpid1g 3560 tpid2g 3562 sssnr 3605 ssprr 3608 sstpr 3609 preqr1 3620 unimax 3695 intmin3 3723 syl6eqbr 3890 pwnss 4002 0inp0 4009 bnd2 4016 exmid01 4040 exmidsssn 4042 exmidundif 4045 exmidundifim 4046 euabex 4063 copsexg 4082 euotd 4092 elopab 4096 epelg 4128 sucidg 4254 regexmidlem1 4364 sucprcreg 4380 onprc 4383 dtruex 4390 omelon2 4437 elvvuni 4517 eqrelriv 4546 relopabi 4578 opabid2 4582 ididg 4604 iss 4773 funopg 5063 fn0 5148 f00 5217 f0bi 5218 f1o00 5303 fo00 5304 brprcneu 5313 relelfvdm 5351 fsn 5485 eufnfv 5541 f1eqcocnv 5586 riotaprop 5647 acexmidlemb 5660 acexmidlemab 5662 acexmidlem2 5665 oprabid 5697 elrnmpt2 5774 ov6g 5798 eqop2 5964 1stconst 6002 2ndconst 6003 dftpos3 6043 dftpos4 6044 2pwuninelg 6064 frecabcl 6180 ecopover 6406 map0g 6461 mapsn 6463 elixpsn 6508 en0 6568 en1 6572 fiprc 6588 dom0 6610 nneneq 6629 findcard 6660 findcard2 6661 findcard2s 6662 sbthlem2 6723 sbthlemi4 6725 sbthlemi5 6726 eldju2ndl 6819 updjudhf 6826 enumct 6849 fodjuomnilemdc 6862 nnnninf 6869 1ne0sr 7375 00sr 7378 eqlei2 7642 divcanap3 8228 nn1suc 8504 nn0ge0 8761 xnn0xr 8804 xnn0nemnf 8810 elnn0z 8826 nn0n0n1ge2b 8889 nn0ind-raph 8926 elnn1uz2 9157 indstr2 9159 xrnemnf 9311 xrnepnf 9312 mnfltxr 9319 nn0pnfge0 9324 xrlttr 9328 xrltso 9329 xrlttri3 9330 nltpnft 9342 ngtmnft 9343 fztpval 9560 fseq1p1m1 9571 fz01or 9588 qbtwnxr 9732 fzfig 9900 uzsinds 9911 iser0f 10011 ser0f 10013 1exp 10047 0exp 10053 bcn1 10229 zfz1iso 10309 sqrt0rlem 10499 0dvds 11157 nn0o 11248 flodddiv4 11275 gcddvds 11296 bezoutlemmain 11328 lcmdvds 11402 rpdvds 11422 1nprm 11437 prmind2 11443 strslfv 11601 restsspw 11725 baspartn 11811 eltg3 11820 topnex 11849 discld 11899 bj-om 12136 bj-nn0suc0 12149 bj-nn0suc 12163 bj-nn0sucALT 12177 bj-findis 12178 el2oss1o 12191 nninfall 12203 |
Copyright terms: Public domain | W3C validator |