Metamath Proof Explorer
Table of Contents - 1.2.11. Abbreviated conjunction and disjunction of three wff's
- w3o
- w3a
- df-3or
- df-3an
- 3orass
- 3orel1
- 3orrot
- 3orcoma
- 3orcomb
- 3anass
- 3anan12
- 3anan32
- 3ancoma
- 3ancomb
- 3anrot
- 3anrev
- anandi3
- anandi3r
- 3anidm
- 3an4anass
- 3ioran
- 3ianor
- 3anor
- 3oran
- 3impa
- 3imp
- 3imp31
- 3imp231
- 3imp21
- 3impb
- 3impib
- 3impia
- 3expa
- 3exp
- 3expb
- 3expia
- 3expib
- 3com12
- 3com13
- 3comr
- 3com23
- 3coml
- 3jca
- 3jcad
- 3adant1
- 3adant2
- 3adant3
- 3ad2ant1
- 3ad2ant2
- 3ad2ant3
- simp1
- simp2
- simp3
- simp1i
- simp2i
- simp3i
- simp1d
- simp2d
- simp3d
- simp1bi
- simp2bi
- simp3bi
- 3simpa
- 3simpb
- 3simpc
- 3anim123i
- 3anim1i
- 3anim2i
- 3anim3i
- 3anbi123i
- 3orbi123i
- 3anbi1i
- 3anbi2i
- 3anbi3i
- syl3an
- syl3anb
- syl3anbr
- syl3an1
- syl3an2
- syl3an3
- 3adantl1
- 3adantl2
- 3adantl3
- 3adantr1
- 3adantr2
- 3adantr3
- ad4ant123
- ad4ant124
- ad4ant134
- ad4ant234
- 3adant1l
- 3adant1r
- 3adant2l
- 3adant2r
- 3adant3l
- 3adant3r
- 3adant3r1
- 3adant3r2
- 3adant3r3
- 3ad2antl1
- 3ad2antl2
- 3ad2antl3
- 3ad2antr1
- 3ad2antr2
- 3ad2antr3
- simpl1
- simpl2
- simpl3
- simpr1
- simpr2
- simpr3
- simp1l
- simp1r
- simp2l
- simp2r
- simp3l
- simp3r
- simp11
- simp12
- simp13
- simp21
- simp22
- simp23
- simp31
- simp32
- simp33
- simpll1
- simpll2
- simpll3
- simplr1
- simplr2
- simplr3
- simprl1
- simprl2
- simprl3
- simprr1
- simprr2
- simprr3
- simpl1l
- simpl1r
- simpl2l
- simpl2r
- simpl3l
- simpl3r
- simpr1l
- simpr1r
- simpr2l
- simpr2r
- simpr3l
- simpr3r
- simp1ll
- simp1lr
- simp1rl
- simp1rr
- simp2ll
- simp2lr
- simp2rl
- simp2rr
- simp3ll
- simp3lr
- simp3rl
- simp3rr
- simpl11
- simpl12
- simpl13
- simpl21
- simpl22
- simpl23
- simpl31
- simpl32
- simpl33
- simpr11
- simpr12
- simpr13
- simpr21
- simpr22
- simpr23
- simpr31
- simpr32
- simpr33
- simp1l1
- simp1l2
- simp1l3
- simp1r1
- simp1r2
- simp1r3
- simp2l1
- simp2l2
- simp2l3
- simp2r1
- simp2r2
- simp2r3
- simp3l1
- simp3l2
- simp3l3
- simp3r1
- simp3r2
- simp3r3
- simp11l
- simp11r
- simp12l
- simp12r
- simp13l
- simp13r
- simp21l
- simp21r
- simp22l
- simp22r
- simp23l
- simp23r
- simp31l
- simp31r
- simp32l
- simp32r
- simp33l
- simp33r
- simp111
- simp112
- simp113
- simp121
- simp122
- simp123
- simp131
- simp132
- simp133
- simp211
- simp212
- simp213
- simp221
- simp222
- simp223
- simp231
- simp232
- simp233
- simp311
- simp312
- simp313
- simp321
- simp322
- simp323
- simp331
- simp332
- simp333
- 3anibar
- 3mix1
- 3mix2
- 3mix3
- 3mix1i
- 3mix2i
- 3mix3i
- 3mix1d
- 3mix2d
- 3mix3d
- 3pm3.2i
- pm3.2an3
- mpbir3an
- mpbir3and
- syl3anbrc
- syl21anbrc
- 3imp3i2an
- ex3
- 3imp1
- 3impd
- 3imp2
- 3impdi
- 3impdir
- 3exp1
- 3expd
- 3exp2
- exp5o
- exp516
- exp520
- 3impexp
- 3an1rs
- 3anassrs
- ad5ant245
- ad5ant234
- ad5ant235
- ad5ant123
- ad5ant124
- ad5ant125
- ad5ant134
- ad5ant135
- ad5ant145
- ad5ant2345
- syl3anc
- syl13anc
- syl31anc
- syl112anc
- syl121anc
- syl211anc
- syl23anc
- syl32anc
- syl122anc
- syl212anc
- syl221anc
- syl113anc
- syl131anc
- syl311anc
- syl33anc
- syl222anc
- syl123anc
- syl132anc
- syl213anc
- syl231anc
- syl312anc
- syl321anc
- syl133anc
- syl313anc
- syl331anc
- syl223anc
- syl232anc
- syl322anc
- syl233anc
- syl323anc
- syl332anc
- syl333anc
- syl3an1b
- syl3an2b
- syl3an3b
- syl3an1br
- syl3an2br
- syl3an3br
- syld3an3
- syld3an1
- syld3an2
- syl3anl1
- syl3anl2
- syl3anl3
- syl3anl
- syl3anr1
- syl3anr2
- syl3anr3
- 3anidm12
- 3anidm13
- 3anidm23
- syl2an3an
- syl2an23an
- 3ori
- 3jao
- 3jaob
- 3jaoi
- 3jaod
- 3jaoian
- 3jaodan
- mpjao3dan
- mpjao3danOLD
- 3jaao
- syl3an9b
- 3orbi123d
- 3anbi123d
- 3anbi12d
- 3anbi13d
- 3anbi23d
- 3anbi1d
- 3anbi2d
- 3anbi3d
- 3anim123d
- 3orim123d
- an6
- 3an6
- 3or6
- mp3an1
- mp3an2
- mp3an3
- mp3an12
- mp3an13
- mp3an23
- mp3an1i
- mp3anl1
- mp3anl2
- mp3anl3
- mp3anr1
- mp3anr2
- mp3anr3
- mp3an
- mpd3an3
- mpd3an23
- mp3and
- mp3an12i
- mp3an2i
- mp3an3an
- mp3an2ani
- biimp3a
- biimp3ar
- 3anandis
- 3anandirs
- ecase23d
- 3ecase
- 3bior1fd
- 3bior1fand
- 3bior2fd
- 3biant1d
- intn3an1d
- intn3an2d
- intn3an3d
- an3andi
- an33rean
- an33reanOLD