![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orim12d | Structured version Visualization version Unicode version |
Description: Disjoin antecedents and consequents in a deduction. (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 845 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2anc 667 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 189 df-or 372 df-an 373 |
This theorem is referenced by: orim1d 851 orim2d 852 3orim123d 1349 preq12b 4154 prel12 4155 fr2nr 4815 sossfld 5286 ordtri3or 5458 funun 5627 soisores 6223 sorpsscmpl 6587 suceloni 6645 ordunisuc2 6676 fnse 6918 oaord 7253 omord2 7273 omcan 7275 oeord 7294 oecan 7295 nnaord 7325 nnmord 7338 omsmo 7360 swoer 7396 unxpwdom 8109 rankxplim3 8357 cdainflem 8626 ackbij2 8678 sornom 8712 fin23lem20 8772 fpwwe2lem10 9069 inatsk 9208 ltadd2 9743 ltord1 10147 ltmul1 10462 lt2msq 10498 mul2lt0bi 11409 xmullem2 11558 difreicc 11771 fzospliti 11957 om2uzlti 12171 om2uzlt2i 12172 om2uzf1oi 12174 absor 13375 ruclem12 14305 dvdslelem 14361 odd2np1lem 14376 odd2np1 14377 isprm6 14678 pythagtrip 14796 pc2dvds 14840 mreexexlem4d 15565 mreexexd 15566 irredrmul 17947 mplsubrglem 18675 znidomb 19144 ppttop 20034 filcon 20910 trufil 20937 ufildr 20958 plycj 23243 cosord 23493 logdivlt 23582 isosctrlem2 23760 atans2 23869 wilthlem2 24006 basellem3 24021 lgsdir2lem4 24266 pntpbnd1 24436 mirhl 24736 axcontlem2 25007 axcontlem4 25009 ex-natded5.13-2 25878 hiidge0 26763 chirredlem4 28058 ifbieq12d2 28171 disjxpin 28210 iocinif 28375 erdszelem11 29936 erdsze2lem2 29939 dfon2lem5 30445 trpredrec 30491 nofv 30556 btwnconn1lem14 30879 btwnconn2 30881 poimir 31985 ispridlc 32315 lcvexchlem4 32615 lcvexchlem5 32616 paddss1 33394 paddss2 33395 rexzrexnn0 35659 pell14qrdich 35727 acongsym 35838 dvdsacongtr 35846 elmod2OLD 38736 propeqop 39009 nn0eo 40439 |
Copyright terms: Public domain | W3C validator |