Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpbiri | GIF 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 8426 sup3exmid 8683 nn1suc 8707 nn0ge0 8970 xnn0xr 9013 xnn0nemnf 9019 elnn0z 9035 nn0n0n1ge2b 9098 nn0ind-raph 9136 elnn1uz2 9369 indstr2 9371 xrnemnf 9532 xrnepnf 9533 mnfltxr 9540 nn0pnfge0 9545 xrlttr 9549 xrltso 9550 xrlttri3 9551 nltpnft 9565 npnflt 9566 ngtmnft 9568 nmnfgt 9569 xsubge0 9632 xposdif 9633 xleaddadd 9638 fztpval 9831 fseq1p1m1 9842 fz01or 9859 qbtwnxr 10003 fzfig 10171 uzsinds 10183 ser0f 10256 1exp 10290 0exp 10296 bcn1 10472 zfz1iso 10552 sqrt0rlem 10743 0dvds 11440 nn0o 11531 flodddiv4 11558 gcddvds 11579 bezoutlemmain 11613 lcmdvds 11687 rpdvds 11707 1nprm 11722 prmind2 11728 ennnfonelemj0 11841 ennnfonelemhf1o 11853 strslfv 11930 restsspw 12057 baspartn 12144 eltg3 12153 topnex 12182 discld 12232 lmreltop 12289 cnpfval 12291 cnprcl2k 12302 idcn 12308 xmet0 12459 blfvalps 12481 blfps 12505 blf 12506 limcimolemlt 12729 recnprss 12752 bj-om 13062 bj-nn0suc0 13075 bj-nn0suc 13089 bj-nn0sucALT 13103 bj-findis 13104 el2oss1o 13115 nninfall 13131 trilpolemcl 13157 |
Copyright terms: Public domain | W3C validator |