![]() |
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-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 1346 dedhb 2822 sbceqal 2932 ssdifeq0 3411 pwidg 3490 elpr2 3515 snidg 3520 exsnrex 3532 rabrsndc 3557 prid1g 3593 tpid1g 3601 tpid2g 3603 sssnr 3646 ssprr 3649 sstpr 3650 preqr1 3661 unimax 3736 intmin3 3764 syl6eqbr 3932 pwnss 4043 0inp0 4050 bnd2 4057 exmid01 4081 exmidsssn 4085 exmidundif 4089 exmidundifim 4090 euabex 4107 copsexg 4126 euotd 4136 elopab 4140 epelg 4172 sucidg 4298 regexmidlem1 4408 sucprcreg 4424 onprc 4427 dtruex 4434 omelon2 4481 elvvuni 4563 eqrelriv 4592 relopabi 4625 opabid2 4630 ididg 4652 iss 4823 funopg 5115 fn0 5200 f00 5272 f0bi 5273 f1o00 5358 fo00 5359 brprcneu 5368 relelfvdm 5407 fsn 5546 eufnfv 5602 f1eqcocnv 5646 riotaprop 5707 acexmidlemb 5720 acexmidlemab 5722 acexmidlem2 5725 oprabid 5757 elrnmpo 5838 ov6g 5862 eqop2 6030 1stconst 6072 2ndconst 6073 dftpos3 6113 dftpos4 6114 2pwuninelg 6134 frecabcl 6250 ecopover 6481 map0g 6536 mapsn 6538 elixpsn 6583 en0 6643 en1 6647 fiprc 6663 dom0 6685 nneneq 6704 findcard 6735 findcard2 6736 findcard2s 6737 sbthlem2 6798 sbthlemi4 6800 sbthlemi5 6801 eldju2ndl 6909 updjudhf 6916 enumct 6952 fodjuomnilemdc 6966 nnnninf 6973 exmidaclem 7012 1ne0sr 7509 00sr 7512 cnm 7567 eqlei2 7781 divcanap3 8371 sup3exmid 8625 nn1suc 8649 nn0ge0 8906 xnn0xr 8949 xnn0nemnf 8955 elnn0z 8971 nn0n0n1ge2b 9034 nn0ind-raph 9072 elnn1uz2 9303 indstr2 9305 xrnemnf 9457 xrnepnf 9458 mnfltxr 9465 nn0pnfge0 9470 xrlttr 9474 xrltso 9475 xrlttri3 9476 nltpnft 9490 npnflt 9491 ngtmnft 9493 nmnfgt 9494 xsubge0 9557 xposdif 9558 xleaddadd 9563 fztpval 9756 fseq1p1m1 9767 fz01or 9784 qbtwnxr 9928 fzfig 10096 uzsinds 10108 ser0f 10181 1exp 10215 0exp 10221 bcn1 10397 zfz1iso 10477 sqrt0rlem 10667 0dvds 11361 nn0o 11452 flodddiv4 11479 gcddvds 11500 bezoutlemmain 11532 lcmdvds 11606 rpdvds 11626 1nprm 11641 prmind2 11647 ennnfonelemj0 11759 ennnfonelemhf1o 11771 strslfv 11846 restsspw 11973 baspartn 12060 eltg3 12069 topnex 12098 discld 12148 lmreltop 12205 cnpfval 12207 cnprcl2k 12217 idcn 12223 xmet0 12352 blfvalps 12374 blfps 12398 blf 12399 limcimolemlt 12589 recnprss 12611 bj-om 12827 bj-nn0suc0 12840 bj-nn0suc 12854 bj-nn0sucALT 12868 bj-findis 12869 el2oss1o 12880 nninfall 12896 trilpolemcl 12922 |
Copyright terms: Public domain | W3C validator |