![]() |
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 1338 | . 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) |
5 | 3jao 1424 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1085 ∧ w3a 1086 |
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 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 |
This theorem is referenced by: 3jaoian 1428 tpres 7204 ordzsl 7838 onzsl 7839 tfrlem16 8399 oawordeulem 8560 fsetexb 8864 elfiun 9431 infsupprpr 9505 domtriomlem 10443 axdc3lem2 10452 rankcf 10778 znegcl 12604 xrltnr 13106 xnegcl 13199 xnegneg 13200 xltnegi 13202 xnegid 13224 xaddrid 13227 xmulrid 13265 xrsupsslem 13293 xrinfmsslem 13294 reltxrnmnf 13328 elfznelfzo 13744 addmodlteq 13918 hashle2pr 14445 hashge2el2difr 14449 hashtpg 14453 hash1to3 14459 swrdnd0 14614 prm23lt5 16754 prm23ge5 16755 cshwshashlem1 17036 01eq0ringOLD 20427 ioombl1 25411 2irrexpq 26579 ppiublem1 27048 zabsle1 27142 gausslemma2dlem0f 27207 gausslemma2dlem0i 27210 gausslemma2dlem4 27215 2lgsoddprm 27262 ostth 27485 sltval2 27502 sltintdifex 27507 sltres 27508 sltsolem1 27521 nosepnelem 27525 nb3grprlem1 29070 pthdivtx 29419 frgr3vlem1 29959 frgr3vlem2 29960 frgrwopreg 30009 frgrregorufr 30011 frgrregord13 30082 kur14lem7 34667 3jaodd 35154 dfrdg2 35237 dfrdg4 35393 iooelexlt 36707 relowlssretop 36708 wl-exeq 36867 iccpartiltu 46549 iccpartigtl 46550 icceuelpart 46563 prproropf1olem4 46633 fmtno4prmfac193 46700 fmtnofz04prm 46704 mogoldbblem 46847 exple2lt6 47203 |
Copyright terms: Public domain | W3C validator |