![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3jaoi | Structured version Visualization version GIF version |
Description: Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.) |
Ref | Expression |
---|---|
3jaoi.1 | ⊢ (𝜑 → 𝜓) |
3jaoi.2 | ⊢ (𝜒 → 𝜓) |
3jaoi.3 | ⊢ (𝜃 → 𝜓) |
Ref | Expression |
---|---|
3jaoi | ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3jaoi.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 3jaoi.2 | . . 3 ⊢ (𝜒 → 𝜓) | |
3 | 3jaoi.3 | . . 3 ⊢ (𝜃 → 𝜓) | |
4 | 1, 2, 3 | 3pm3.2i 1336 | . 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) |
5 | 3jao 1422 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1083 ∧ w3a 1084 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 |
This theorem is referenced by: 3jaoian 1426 tpres 6940 ordzsl 7540 onzsl 7541 tfrlem16 8012 oawordeulem 8163 elfiun 8878 infsupprpr 8952 domtriomlem 9853 axdc3lem2 9862 rankcf 10188 znegcl 12005 xrltnr 12502 xnegcl 12594 xnegneg 12595 xltnegi 12597 xnegid 12619 xaddid1 12622 xmulid1 12660 xrsupsslem 12688 xrinfmsslem 12689 reltxrnmnf 12723 elfznelfzo 13137 addmodlteq 13309 hashle2pr 13831 hashge2el2difr 13835 hashtpg 13839 hash1to3 13845 swrdnd0 14010 prm23lt5 16141 prm23ge5 16142 cshwshashlem1 16421 01eq0ring 20038 ioombl1 24166 2irrexpq 25321 ppiublem1 25786 zabsle1 25880 gausslemma2dlem0f 25945 gausslemma2dlem0i 25948 gausslemma2dlem4 25953 2lgsoddprm 26000 ostth 26223 nb3grprlem1 27170 pthdivtx 27518 frgr3vlem1 28058 frgr3vlem2 28059 frgrwopreg 28108 frgrregorufr 28110 frgrregord13 28181 kur14lem7 32572 3jaodd 33057 dfrdg2 33153 sltval2 33276 sltintdifex 33281 sltres 33282 sltsolem1 33293 nosepnelem 33297 dfrdg4 33525 iooelexlt 34779 relowlssretop 34780 wl-exeq 34939 iccpartiltu 43939 iccpartigtl 43940 icceuelpart 43953 prproropf1olem4 44023 fmtno4prmfac193 44090 fmtnofz04prm 44094 mogoldbblem 44238 exple2lt6 44766 |
Copyright terms: Public domain | W3C validator |