![]() |
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 1320 | . 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) |
5 | 3jao 1406 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1068 ∧ w3a 1069 |
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 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 |
This theorem is referenced by: 3jaoian 1410 tpres 6789 ordzsl 7375 onzsl 7376 tfrlem16 7832 oawordeulem 7980 elfiun 8688 infsupprpr 8762 domtriomlem 9661 axdc3lem2 9670 rankcf 9996 znegcl 11829 xrltnr 12330 xnegcl 12422 xnegneg 12423 xltnegi 12425 xnegid 12447 xaddid1 12450 xmulid1 12487 xrsupsslem 12515 xrinfmsslem 12516 reltxrnmnf 12550 elfznelfzo 12956 addmodlteq 13128 hashle2pr 13645 hashge2el2difr 13649 hashtpg 13653 hash1to3 13659 swrdnd0 13824 prm23lt5 16006 prm23ge5 16007 cshwshashlem1 16284 01eq0ring 19779 ioombl1 23882 2irrexpq 25030 ppiublem1 25496 zabsle1 25590 gausslemma2dlem0f 25655 gausslemma2dlem0i 25658 gausslemma2dlem4 25663 2lgsoddprm 25710 ostth 25933 nb3grprlem1 26881 pthdivtx 27234 frgr3vlem1 27823 frgr3vlem2 27824 frgrwopreg 27873 frgrregorufr 27875 frgrregord13 27969 kur14lem7 32077 3jaodd 32497 dfrdg2 32594 sltval2 32717 sltintdifex 32722 sltres 32723 sltsolem1 32734 nosepnelem 32738 dfrdg4 32966 iooelexlt 34118 relowlssretop 34119 wl-exeq 34249 iccpartiltu 42984 iccpartigtl 42985 icceuelpart 42998 prproropf1olem4 43066 fmtno4prmfac193 43133 fmtnofz04prm 43137 mogoldbblem 43283 exple2lt6 43808 |
Copyright terms: Public domain | W3C validator |