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 1341 | . 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) |
5 | 3jao 1427 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1088 ∧ w3a 1089 |
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 848 df-3or 1090 df-3an 1091 |
This theorem is referenced by: 3jaoian 1431 tpres 7038 ordzsl 7646 onzsl 7647 tfrlem16 8153 oawordeulem 8306 fsetexb 8569 elfiun 9076 infsupprpr 9150 domtriomlem 10086 axdc3lem2 10095 rankcf 10421 znegcl 12242 xrltnr 12741 xnegcl 12833 xnegneg 12834 xltnegi 12836 xnegid 12858 xaddid1 12861 xmulid1 12899 xrsupsslem 12927 xrinfmsslem 12928 reltxrnmnf 12962 elfznelfzo 13377 addmodlteq 13551 hashle2pr 14076 hashge2el2difr 14080 hashtpg 14084 hash1to3 14090 swrdnd0 14255 prm23lt5 16400 prm23ge5 16401 cshwshashlem1 16682 01eq0ring 20343 ioombl1 24491 2irrexpq 25650 ppiublem1 26115 zabsle1 26209 gausslemma2dlem0f 26274 gausslemma2dlem0i 26277 gausslemma2dlem4 26282 2lgsoddprm 26329 ostth 26552 nb3grprlem1 27500 pthdivtx 27848 frgr3vlem1 28388 frgr3vlem2 28389 frgrwopreg 28438 frgrregorufr 28440 frgrregord13 28511 kur14lem7 32918 3jaodd 33403 dfrdg2 33521 sltval2 33630 sltintdifex 33635 sltres 33636 sltsolem1 33649 nosepnelem 33653 dfrdg4 34024 iooelexlt 35307 relowlssretop 35308 wl-exeq 35467 iccpartiltu 44593 iccpartigtl 44594 icceuelpart 44607 prproropf1olem4 44677 fmtno4prmfac193 44744 fmtnofz04prm 44748 mogoldbblem 44891 exple2lt6 45419 |
Copyright terms: Public domain | W3C validator |