![]() |
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 167 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm5.18im 1396 dedhb 2921 sbceqal 3033 ssdifeq0 3520 pwidg 3604 elpr2 3629 snidg 3636 exsnrex 3649 rabrsndc 3675 prid1g 3711 tpid1g 3719 tpid2g 3721 sssnr 3768 ssprr 3771 sstpr 3772 preqr1 3783 unimax 3858 intmin3 3886 eqbrtrdi 4057 pwnss 4177 0inp0 4184 bnd2 4191 ss1o0el1 4215 exmidsssn 4220 exmidundif 4224 exmidundifim 4225 euabex 4243 copsexg 4262 euotd 4272 elopab 4276 epelg 4308 sucidg 4434 ifelpwung 4499 regexmidlem1 4550 sucprcreg 4566 onprc 4569 dtruex 4576 omelon2 4625 elvvuni 4708 eqrelriv 4737 relopabi 4770 opabid2 4776 ididg 4798 iss 4971 funopg 5269 fn0 5354 f00 5426 f0bi 5427 f1o00 5515 fo00 5516 brprcneu 5527 relelfvdm 5566 fsn 5708 eufnfv 5767 f1eqcocnv 5812 riotaprop 5874 acexmidlemb 5887 acexmidlemab 5889 acexmidlem2 5892 oprabid 5927 elrnmpo 6009 ov6g 6033 eqop2 6202 1stconst 6245 2ndconst 6246 dftpos3 6286 dftpos4 6287 2pwuninelg 6307 frecabcl 6423 el2oss1o 6467 ecopover 6658 map0g 6713 mapsn 6715 elixpsn 6760 en0 6820 en1 6824 fiprc 6840 dom0 6865 nneneq 6884 findcard 6915 findcard2 6916 findcard2s 6917 sbthlem2 6986 sbthlemi4 6988 sbthlemi5 6989 eldju2ndl 7100 updjudhf 7107 enumct 7143 nnnninf 7153 nninfisollem0 7157 fodjuomnilemdc 7171 exmidonfinlem 7221 exmidaclem 7236 pw1ne1 7257 pw1ne3 7258 1ne0sr 7794 00sr 7797 cnm 7860 eqlei2 8081 cnstab 8631 divcanap3 8684 sup3exmid 8943 nn1suc 8967 nn0ge0 9230 xnn0xr 9273 xnn0nemnf 9279 elnn0z 9295 nn0n0n1ge2b 9361 nn0ind-raph 9399 elnn1uz2 9636 indstr2 9638 xrnemnf 9806 xrnepnf 9807 mnfltxr 9815 nn0pnfge0 9820 xrlttr 9824 xrltso 9825 xrlttri3 9826 nltpnft 9843 npnflt 9844 ngtmnft 9846 nmnfgt 9847 xsubge0 9910 xposdif 9911 xleaddadd 9916 fztpval 10112 fseq1p1m1 10123 fz01or 10140 qbtwnxr 10287 xqltnle 10297 fzfig 10460 uzsinds 10472 ser0f 10545 1exp 10579 0exp 10585 bcn1 10769 zfz1iso 10852 sqrt0rlem 11043 prodf1f 11582 0dvds 11849 nn0o 11943 flodddiv4 11970 gcddvds 11995 bezoutlemmain 12030 lcmdvds 12110 rpdvds 12130 1nprm 12145 prmind2 12151 nnoddn2prmb 12293 pcpre1 12323 qexpz 12383 4sqlem19 12440 ennnfonelemj0 12451 ennnfonelemhf1o 12463 strslfv 12556 restsspw 12751 xpsfrnel 12817 mgmidcl 12851 mgmlrid 12852 releqgg 13156 islidlm 13792 zrhrhm 13917 baspartn 14002 eltg3 14009 topnex 14038 discld 14088 lmreltop 14145 cnpfval 14147 cnprcl2k 14158 idcn 14164 xmet0 14315 blfvalps 14337 blfps 14361 blf 14362 limcimolemlt 14585 recnprss 14608 lgsdir2lem2 14883 2sqlem7 14921 funmptd 15008 bj-om 15142 bj-nn0suc0 15155 bj-nn0suc 15169 bj-nn0sucALT 15183 bj-findis 15184 nninfall 15212 trilpolemcl 15239 dceqnconst 15262 dcapnconst 15263 |
Copyright terms: Public domain | W3C validator |