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: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 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 1348 dedhb 2826 sbceqal 2936 ssdifeq0 3415 pwidg 3494 elpr2 3519 snidg 3524 exsnrex 3536 rabrsndc 3561 prid1g 3597 tpid1g 3605 tpid2g 3607 sssnr 3650 ssprr 3653 sstpr 3654 preqr1 3665 unimax 3740 intmin3 3768 eqbrtrdi 3937 pwnss 4053 0inp0 4060 bnd2 4067 exmid01 4091 exmidsssn 4095 exmidundif 4099 exmidundifim 4100 euabex 4117 copsexg 4136 euotd 4146 elopab 4150 epelg 4182 sucidg 4308 regexmidlem1 4418 sucprcreg 4434 onprc 4437 dtruex 4444 omelon2 4491 elvvuni 4573 eqrelriv 4602 relopabi 4635 opabid2 4640 ididg 4662 iss 4835 funopg 5127 fn0 5212 f00 5284 f0bi 5285 f1o00 5370 fo00 5371 brprcneu 5382 relelfvdm 5421 fsn 5560 eufnfv 5616 f1eqcocnv 5660 riotaprop 5721 acexmidlemb 5734 acexmidlemab 5736 acexmidlem2 5739 oprabid 5771 elrnmpo 5852 ov6g 5876 eqop2 6044 1stconst 6086 2ndconst 6087 dftpos3 6127 dftpos4 6128 2pwuninelg 6148 frecabcl 6264 ecopover 6495 map0g 6550 mapsn 6552 elixpsn 6597 en0 6657 en1 6661 fiprc 6677 dom0 6700 nneneq 6719 findcard 6750 findcard2 6751 findcard2s 6752 sbthlem2 6814 sbthlemi4 6816 sbthlemi5 6817 eldju2ndl 6925 updjudhf 6932 enumct 6968 fodjuomnilemdc 6984 nnnninf 6991 exmidonfinlem 7017 exmidaclem 7032 1ne0sr 7542 00sr 7545 cnm 7608 eqlei2 7826 divcanap3 8425 sup3exmid 8679 nn1suc 8703 nn0ge0 8960 xnn0xr 9003 xnn0nemnf 9009 elnn0z 9025 nn0n0n1ge2b 9088 nn0ind-raph 9126 elnn1uz2 9357 indstr2 9359 xrnemnf 9519 xrnepnf 9520 mnfltxr 9527 nn0pnfge0 9532 xrlttr 9536 xrltso 9537 xrlttri3 9538 nltpnft 9552 npnflt 9553 ngtmnft 9555 nmnfgt 9556 xsubge0 9619 xposdif 9620 xleaddadd 9625 fztpval 9818 fseq1p1m1 9829 fz01or 9846 qbtwnxr 9990 fzfig 10158 uzsinds 10170 ser0f 10243 1exp 10277 0exp 10283 bcn1 10459 zfz1iso 10539 sqrt0rlem 10730 0dvds 11425 nn0o 11516 flodddiv4 11543 gcddvds 11564 bezoutlemmain 11598 lcmdvds 11672 rpdvds 11692 1nprm 11707 prmind2 11713 ennnfonelemj0 11825 ennnfonelemhf1o 11837 strslfv 11914 restsspw 12041 baspartn 12128 eltg3 12137 topnex 12166 discld 12216 lmreltop 12273 cnpfval 12275 cnprcl2k 12286 idcn 12292 xmet0 12443 blfvalps 12465 blfps 12489 blf 12490 limcimolemlt 12713 recnprss 12736 bj-om 13031 bj-nn0suc0 13044 bj-nn0suc 13058 bj-nn0sucALT 13072 bj-findis 13073 el2oss1o 13084 nninfall 13100 trilpolemcl 13126 |
Copyright terms: Public domain | W3C validator |