![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orim12d | Structured version Visualization version GIF version |
Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 936 for a proof which does not depend on df-an 386. (Contributed by NM, 10-May-1994.) |
Ref | Expression |
---|---|
orim12d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
orim12d.2 | ⊢ (𝜑 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
orim12d | ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orim12d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | orim12d.2 | . 2 ⊢ (𝜑 → (𝜃 → 𝜏)) | |
3 | pm3.48 987 | . 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) | |
4 | 1, 2, 3 | syl2anc 580 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 874 |
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 386 df-or 875 |
This theorem is referenced by: orim1d 989 orim2d 990 3orim123d 1569 preq12b 4567 prel12OLD 4568 propeqop 5163 fr2nr 5290 sossfld 5797 ordtri3or 5973 ordelinel 6039 funun 6146 soisores 6805 sorpsscmpl 7182 suceloni 7247 ordunisuc2 7278 fnse 7531 oaord 7867 omord2 7887 omcan 7889 oeord 7908 oecan 7909 nnaord 7939 nnmord 7952 omsmo 7974 swoer 8012 unxpwdom 8736 rankxplim3 8994 cdainflem 9301 ackbij2 9353 sornom 9387 fin23lem20 9447 fpwwe2lem10 9749 inatsk 9888 ltadd2 10431 ltord1 10846 ltmul1 11165 lt2msq 11200 mul2lt0bi 12181 xmullem2 12344 difreicc 12558 fzospliti 12755 om2uzlti 13004 om2uzlt2i 13005 om2uzf1oi 13007 absor 14381 ruclem12 15306 dvdslelem 15370 odd2np1lem 15400 odd2np1 15401 isprm6 15759 pythagtrip 15872 pc2dvds 15916 mreexexlem4d 16622 mreexexd 16623 irredrmul 19023 mplsubrglem 19762 znidomb 20231 ppttop 21140 filconn 22015 trufil 22042 ufildr 22063 plycj 24374 cosord 24620 logdivlt 24708 isosctrlem2 24901 atans2 25010 wilthlem2 25147 basellem3 25161 lgsdir2lem4 25405 pntpbnd1 25627 mirhl 25930 axcontlem2 26202 axcontlem4 26204 ex-natded5.13-2 27801 hiidge0 28480 chirredlem4 29777 disjxpin 29918 iocinif 30061 erdszelem11 31700 erdsze2lem2 31703 dfon2lem5 32204 trpredrec 32250 nofv 32323 nolesgn2o 32337 btwnconn1lem14 32720 btwnconn2 32722 poimir 33931 ispridlc 34356 lcvexchlem4 35058 lcvexchlem5 35059 paddss1 35838 paddss2 35839 rexzrexnn0 38154 pell14qrdich 38219 acongsym 38328 dvdsacongtr 38336 or3or 39101 clsk1indlem3 39123 nn0eo 43121 |
Copyright terms: Public domain | W3C validator |