![]() |
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 1385 dedhb 2907 sbceqal 3019 ssdifeq0 3506 pwidg 3590 elpr2 3615 snidg 3622 exsnrex 3635 rabrsndc 3661 prid1g 3697 tpid1g 3705 tpid2g 3707 sssnr 3754 ssprr 3757 sstpr 3758 preqr1 3769 unimax 3844 intmin3 3872 eqbrtrdi 4043 pwnss 4160 0inp0 4167 bnd2 4174 ss1o0el1 4198 exmidsssn 4203 exmidundif 4207 exmidundifim 4208 euabex 4226 copsexg 4245 euotd 4255 elopab 4259 epelg 4291 sucidg 4417 ifelpwung 4482 regexmidlem1 4533 sucprcreg 4549 onprc 4552 dtruex 4559 omelon2 4608 elvvuni 4691 eqrelriv 4720 relopabi 4753 opabid2 4759 ididg 4781 iss 4954 funopg 5251 fn0 5336 f00 5408 f0bi 5409 f1o00 5497 fo00 5498 brprcneu 5509 relelfvdm 5548 fsn 5689 eufnfv 5748 f1eqcocnv 5792 riotaprop 5854 acexmidlemb 5867 acexmidlemab 5869 acexmidlem2 5872 oprabid 5907 elrnmpo 5988 ov6g 6012 eqop2 6179 1stconst 6222 2ndconst 6223 dftpos3 6263 dftpos4 6264 2pwuninelg 6284 frecabcl 6400 el2oss1o 6444 ecopover 6633 map0g 6688 mapsn 6690 elixpsn 6735 en0 6795 en1 6799 fiprc 6815 dom0 6838 nneneq 6857 findcard 6888 findcard2 6889 findcard2s 6890 sbthlem2 6957 sbthlemi4 6959 sbthlemi5 6960 eldju2ndl 7071 updjudhf 7078 enumct 7114 nnnninf 7124 nninfisollem0 7128 fodjuomnilemdc 7142 exmidonfinlem 7192 exmidaclem 7207 pw1ne1 7228 pw1ne3 7229 1ne0sr 7765 00sr 7768 cnm 7831 eqlei2 8052 cnstab 8602 divcanap3 8655 sup3exmid 8914 nn1suc 8938 nn0ge0 9201 xnn0xr 9244 xnn0nemnf 9250 elnn0z 9266 nn0n0n1ge2b 9332 nn0ind-raph 9370 elnn1uz2 9607 indstr2 9609 xrnemnf 9777 xrnepnf 9778 mnfltxr 9786 nn0pnfge0 9791 xrlttr 9795 xrltso 9796 xrlttri3 9797 nltpnft 9814 npnflt 9815 ngtmnft 9817 nmnfgt 9818 xsubge0 9881 xposdif 9882 xleaddadd 9887 fztpval 10083 fseq1p1m1 10094 fz01or 10111 qbtwnxr 10258 fzfig 10430 uzsinds 10442 ser0f 10515 1exp 10549 0exp 10555 bcn1 10738 zfz1iso 10821 sqrt0rlem 11012 prodf1f 11551 0dvds 11818 nn0o 11912 flodddiv4 11939 gcddvds 11964 bezoutlemmain 11999 lcmdvds 12079 rpdvds 12099 1nprm 12114 prmind2 12120 nnoddn2prmb 12262 pcpre1 12292 qexpz 12350 ennnfonelemj0 12402 ennnfonelemhf1o 12414 strslfv 12507 restsspw 12698 xpsfrnel 12763 mgmidcl 12797 mgmlrid 12798 releqgg 13080 baspartn 13553 eltg3 13560 topnex 13589 discld 13639 lmreltop 13696 cnpfval 13698 cnprcl2k 13709 idcn 13715 xmet0 13866 blfvalps 13888 blfps 13912 blf 13913 limcimolemlt 14136 recnprss 14159 lgsdir2lem2 14433 2sqlem7 14471 funmptd 14558 bj-om 14692 bj-nn0suc0 14705 bj-nn0suc 14719 bj-nn0sucALT 14733 bj-findis 14734 nninfall 14761 trilpolemcl 14788 dceqnconst 14810 dcapnconst 14811 |
Copyright terms: Public domain | W3C validator |