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 1331 | . 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) |
5 | 3jao 1417 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1078 ∧ w3a 1079 |
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 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 |
This theorem is referenced by: 3jaoian 1421 tpres 6956 ordzsl 7548 onzsl 7549 tfrlem16 8020 oawordeulem 8170 elfiun 8883 infsupprpr 8957 domtriomlem 9853 axdc3lem2 9862 rankcf 10188 znegcl 12006 xrltnr 12504 xnegcl 12596 xnegneg 12597 xltnegi 12599 xnegid 12621 xaddid1 12624 xmulid1 12662 xrsupsslem 12690 xrinfmsslem 12691 reltxrnmnf 12725 elfznelfzo 13132 addmodlteq 13304 hashle2pr 13825 hashge2el2difr 13829 hashtpg 13833 hash1to3 13839 swrdnd0 14009 prm23lt5 16141 prm23ge5 16142 cshwshashlem1 16419 01eq0ring 19975 ioombl1 24092 2irrexpq 25240 ppiublem1 25706 zabsle1 25800 gausslemma2dlem0f 25865 gausslemma2dlem0i 25868 gausslemma2dlem4 25873 2lgsoddprm 25920 ostth 26143 nb3grprlem1 27090 pthdivtx 27438 frgr3vlem1 27980 frgr3vlem2 27981 frgrwopreg 28030 frgrregorufr 28032 frgrregord13 28103 kur14lem7 32357 3jaodd 32842 dfrdg2 32938 sltval2 33061 sltintdifex 33066 sltres 33067 sltsolem1 33078 nosepnelem 33082 dfrdg4 33310 iooelexlt 34526 relowlssretop 34527 wl-exeq 34656 iccpartiltu 43429 iccpartigtl 43430 icceuelpart 43443 prproropf1olem4 43515 fmtno4prmfac193 43582 fmtnofz04prm 43586 mogoldbblem 43732 exple2lt6 44310 |
Copyright terms: Public domain | W3C validator |