3 ms·

Only the 5th is true, Metamath: $( <MM> <PROOF_ASST> THEOREM=noneabove LOC_AFTER=? h50::noneabove.1 |- ( ph <-> ( ( ps /\ ch /\ th ) /\ ( ta /\ et ) ) ) h5

by mazsa 7y ago

Only the 5th is true, Metamath: $( <MM> <PROOF_ASST> THEOREM=noneabove LOC_AFTER=? h50::noneabove.1 |- ( ph <-> ( ( ps /\ ch /\ th ) /\ ( ta /\ et ) ) ) h51::noneabove.2 |- ( ps <-> ( -. ch /\ ( -. th /\ -. ta ) /\ -. et ) ) h52::noneabove.3 |- ( ch <-> ( ph /\ ps ) ) h53::noneabove.4 |- ( th <-> ( ph \/ ps \/ ch ) ) h54::noneabove.5 |- ( ta <-> ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) ) h55::noneabove.6 |- ( et <-> ( ( -. ph /\ -. ps /\ -. ch ) /\ ( -. th /\ -. ta ) ) ) 56:50:simprbi |- ( ph -> ( ta /\ et ) ) 57:56:simprd |- ( ph -> et ) 58:51:simp3bi |- ( ps -> -. et ) 59:57,58:anim12i |- ( ( ph /\ ps ) -> ( et /\ -. et ) ) 60::pm3.24 |- -. ( et /\ -. et ) 61:60,59:mto |- -. ( ph /\ ps ) 62:61,52:mtbir |- -. ch 63:50:simplbi |- ( ph -> ( ps /\ ch /\ th ) ) 64:63:simp2d |- ( ph -> ch ) 65:62,64:mto |- -. ph 66::3ioran |- ( -. ( ph \/ ps \/ ch ) <-> ( -. ph /\ -. ps /\ -. ch ) ) 67:53:notbii |- ( -. th <-> -. ( ph \/ ps \/ ch ) ) 68:67,66:bitri |- ( -. th <-> ( -. ph /\ -. ps /\ -. ch ) ) 69:68:anbi1i |- ( ( -. th /\ -. th ) <-> ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) ) 70::pm4.24 |- ( -. th <-> ( -. th /\ -. th ) ) 71:69,70,54:3bitr4i |- ( -. th <-> ta ) 72::nbbn |- ( ( -. th <-> ta ) <-> -. ( th <-> ta ) ) 73:71,72:mpbi |- -. ( th <-> ta ) 74::df-xor |- ( ( th \/_ ta ) <-> -. ( th <-> ta ) ) 75:73,74:mpbir |- ( th \/_ ta ) 76::xoror |- ( ( th \/_ ta ) -> ( th \/ ta ) ) 77:75,76:ax-mp |- ( th \/ ta ) 78:55:simprbi |- ( et -> ( -. th /\ -. ta ) ) 79::pm4.56 |- ( ( -. th /\ -. ta ) <-> -. ( th \/ ta ) ) 80:78,79:sylib |- ( et -> -. ( th \/ ta ) ) 81:77,80:mt2 |- -. et 82:51:simp2bi |- ( ps -> ( -. th /\ -. ta ) ) 83::pm4.56 |- ( ( -. th /\ -. ta ) <-> -. ( th \/ ta ) ) 84:82,83:sylib |- ( ps -> -. ( th \/ ta ) ) 85:77,84:mt2 |- -. ps 86:65,85,62:3pm3.2ni |- -. ( ph \/ ps \/ ch ) 87:86,53:mtbir |- -. th 88:87,75:mtpxor |- ta 89:65,85,62:3pm3.2i |- ( -. ph /\ -. ps /\ -. ch ) 90:89,87:pm3.2i |- ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) qed:90,88,81:3pm3.2i |- ( ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) /\ ta /\ -. et ) $= ( w3a simprbi mto wn wa mtbir wb sylib mt2 3pm3.2i pm3.24 simprd simp2d simp3bi anim12i simplbi wo notbii 3ioran bitri anbi1i wxo w3o pm4.24 3bitr4i nbbn mpbi df-xor mpbir xoror ax-mp simp2bi pm4.56 3pm3.2ni pm3.2i mtpxor ) ANZBNZCNZKZDNZOZEFNZVLVMVIVJVKACC ABOZVPFVOOFUBAFBVOAEFABCDKZEFOZGLUCBVKVMENOZVOHUFUGMIPZABCDAVQVRG UHUDMZBDEUIZDEUNZWBWCDEQNZVMEQWDVMVMOVNVMEVMVLVMVMABCUOZNVLDWEJUJ ABCUKULUMVMUPUAUQDEURUSDEUTVAZDEVBVCZBVSWBNZBVKVSVOHVDDEVEZRSZVTT DWEABCWAWJVTVFJPZVGDEWKWFVHFWBWGFVSWHFVLVSUELWIRST $. $)

mazsa 7y ago
Although h53::noneabove.4 |- ( th <-> ( ph \/ ps \/ ch ) ) is not a correct interpretation of "[Exactly] One of the above", it is rather "[At least] One of the above", it doesn't matter because 'th' is not true anyway.
jansan 7y ago
I didn't expect it to be that easy to solve :)
gowld 7y ago
Is this readable with more linebreaks?
- mazsa 7y ago
  Not editable anymore but here you are (cf. http://us.metamath.org/metamath/set.mm http://us.metamath.org/metamath/set.mm ) : h50::noneabove.1 |- ( ph <-> ( ( ps /\ ch /\ th ) /\ ( ta /\ et ) ) ) h51::noneabove.2 |- ( ps <-> ( -. ch /\ ( -. th /\ -. ta ) /\ -. et ) ) h52::noneabove.3 |- ( ch <-> ( ph /\ ps ) ) h53::noneabove.4 |- ( th <-> ( ph \/ ps \/ ch ) ) h54::noneabove.5 |- ( ta <-> ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) ) h55::noneabove.6 |- ( et <-> ( ( -. ph /\ -. ps /\ -. ch ) /\ ( -. th /\ -. ta ) ) ) 56:50:simprbi |- ( ph -> ( ta /\ et ) ) 57:56:simprd |- ( ph -> et ) 58:51:simp3bi |- ( ps -> -. et ) 59:57,58:anim12i |- ( ( ph /\ ps ) -> ( et /\ -. et ) ) 60::pm3.24 |- -. ( et /\ -. et ) 61:60,59:mto |- -. ( ph /\ ps ) 62:61,52:mtbir |- -. ch 63:50:simplbi |- ( ph -> ( ps /\ ch /\ th ) ) 64:63:simp2d |- ( ph -> ch ) 65:62,64:mto |- -. ph 66::3ioran |- ( -. ( ph \/ ps \/ ch ) <-> ( -. ph /\ -. ps /\ -. ch ) ) 67:53:notbii |- ( -. th <-> -. ( ph \/ ps \/ ch ) ) 68:67,66:bitri |- ( -. th <-> ( -. ph /\ -. ps /\ -. ch ) ) 69:68:anbi1i |- ( ( -. th /\ -. th ) <-> ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) ) 70::pm4.24 |- ( -. th <-> ( -. th /\ -. th ) ) 71:69,70,54:3bitr4i |- ( -. th <-> ta ) 72::nbbn |- ( ( -. th <-> ta ) <-> -. ( th <-> ta ) ) 73:71,72:mpbi |- -. ( th <-> ta ) 74::df-xor |- ( ( th \/_ ta ) <-> -. ( th <-> ta ) ) 75:73,74:mpbir |- ( th \/_ ta ) 76::xoror |- ( ( th \/_ ta ) -> ( th \/ ta ) ) 77:75,76:ax-mp |- ( th \/ ta ) 78:55:simprbi |- ( et -> ( -. th /\ -. ta ) ) 79::pm4.56 |- ( ( -. th /\ -. ta ) <-> -. ( th \/ ta ) ) 80:78,79:sylib |- ( et -> -. ( th \/ ta ) ) 81:77,80:mt2 |- -. et 82:51:simp2bi |- ( ps -> ( -. th /\ -. ta ) ) 83::pm4.56 |- ( ( -. th /\ -. ta ) <-> -. ( th \/ ta ) ) 84:82,83:sylib |- ( ps -> -. ( th \/ ta ) ) 85:77,84:mt2 |- -. ps 86:65,85,62:3pm3.2ni |- -. ( ph \/ ps \/ ch ) 87:86,53:mtbir |- -. th 88:87,75:mtpxor |- ta 89:65,85,62:3pm3.2i |- ( -. ph /\ -. ps /\ -. ch ) 90:89,87:pm3.2i |- ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) qed:90,88,81:3pm3.2i |- ( ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) /\ ta /\ -. et )

by mazsa 7y ago

mazsa 7y ago

Although h53::noneabove.4 |- ( th <-> ( ph \/ ps \/ ch ) ) is not a correct interpretation of "[Exactly] One of the above", it is rather "[At least] One of the above", it doesn't matter because 'th' is not true anyway.

jansan 7y ago

I didn't expect it to be that easy to solve :)

gowld 7y ago

Is this readable with more linebreaks?

mazsa 7y ago
Not editable anymore but here you are (cf. http://us.metamath.org/metamath/set.mm http://us.metamath.org/metamath/set.mm ) : h50::noneabove.1 |- ( ph <-> ( ( ps /\ ch /\ th ) /\ ( ta /\ et ) ) ) h51::noneabove.2 |- ( ps <-> ( -. ch /\ ( -. th /\ -. ta ) /\ -. et ) ) h52::noneabove.3 |- ( ch <-> ( ph /\ ps ) ) h53::noneabove.4 |- ( th <-> ( ph \/ ps \/ ch ) ) h54::noneabove.5 |- ( ta <-> ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) ) h55::noneabove.6 |- ( et <-> ( ( -. ph /\ -. ps /\ -. ch ) /\ ( -. th /\ -. ta ) ) ) 56:50:simprbi |- ( ph -> ( ta /\ et ) ) 57:56:simprd |- ( ph -> et ) 58:51:simp3bi |- ( ps -> -. et ) 59:57,58:anim12i |- ( ( ph /\ ps ) -> ( et /\ -. et ) ) 60::pm3.24 |- -. ( et /\ -. et ) 61:60,59:mto |- -. ( ph /\ ps ) 62:61,52:mtbir |- -. ch 63:50:simplbi |- ( ph -> ( ps /\ ch /\ th ) ) 64:63:simp2d |- ( ph -> ch ) 65:62,64:mto |- -. ph 66::3ioran |- ( -. ( ph \/ ps \/ ch ) <-> ( -. ph /\ -. ps /\ -. ch ) ) 67:53:notbii |- ( -. th <-> -. ( ph \/ ps \/ ch ) ) 68:67,66:bitri |- ( -. th <-> ( -. ph /\ -. ps /\ -. ch ) ) 69:68:anbi1i |- ( ( -. th /\ -. th ) <-> ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) ) 70::pm4.24 |- ( -. th <-> ( -. th /\ -. th ) ) 71:69,70,54:3bitr4i |- ( -. th <-> ta ) 72::nbbn |- ( ( -. th <-> ta ) <-> -. ( th <-> ta ) ) 73:71,72:mpbi |- -. ( th <-> ta ) 74::df-xor |- ( ( th \/_ ta ) <-> -. ( th <-> ta ) ) 75:73,74:mpbir |- ( th \/_ ta ) 76::xoror |- ( ( th \/_ ta ) -> ( th \/ ta ) ) 77:75,76:ax-mp |- ( th \/ ta ) 78:55:simprbi |- ( et -> ( -. th /\ -. ta ) ) 79::pm4.56 |- ( ( -. th /\ -. ta ) <-> -. ( th \/ ta ) ) 80:78,79:sylib |- ( et -> -. ( th \/ ta ) ) 81:77,80:mt2 |- -. et 82:51:simp2bi |- ( ps -> ( -. th /\ -. ta ) ) 83::pm4.56 |- ( ( -. th /\ -. ta ) <-> -. ( th \/ ta ) ) 84:82,83:sylib |- ( ps -> -. ( th \/ ta ) ) 85:77,84:mt2 |- -. ps 86:65,85,62:3pm3.2ni |- -. ( ph \/ ps \/ ch ) 87:86,53:mtbir |- -. th 88:87,75:mtpxor |- ta 89:65,85,62:3pm3.2i |- ( -. ph /\ -. ps /\ -. ch ) 90:89,87:pm3.2i |- ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) qed:90,88,81:3pm3.2i |- ( ( ( -. ph /\ -. ps /\ -. ch ) /\ -. th ) /\ ta /\ -. et )