MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orim12d Structured version   Visualization version   GIF version

Theorem orim12d 878
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
Hypotheses
Ref Expression
orim12d.1 (𝜑 → (𝜓𝜒))
orim12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
orim12d (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))

Proof of Theorem orim12d
StepHypRef Expression
1 orim12d.1 . 2 (𝜑 → (𝜓𝜒))
2 orim12d.2 . 2 (𝜑 → (𝜃𝜏))
3 pm3.48 873 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → ((𝜓𝜃) → (𝜒𝜏)))
41, 2, 3syl2anc 690 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381
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 195  df-or 383  df-an 384
This theorem is referenced by:  orim1d  879  orim2d  880  3orim123d  1398  preq12b  4314  prel12  4315  fr2nr  5003  sossfld  5482  ordtri3or  5655  ordelinel  5725  funun  5829  soisores  6452  sorpsscmpl  6820  suceloni  6879  ordunisuc2  6910  fnse  7155  oaord  7488  omord2  7508  omcan  7510  oeord  7529  oecan  7530  nnaord  7560  nnmord  7573  omsmo  7595  swoer  7633  unxpwdom  8351  rankxplim3  8601  cdainflem  8870  ackbij2  8922  sornom  8956  fin23lem20  9016  fpwwe2lem10  9314  inatsk  9453  ltadd2  9989  ltord1  10400  ltmul1  10719  lt2msq  10754  mul2lt0bi  11765  xmullem2  11921  difreicc  12128  fzospliti  12321  om2uzlti  12563  om2uzlt2i  12564  om2uzf1oi  12566  absor  13831  ruclem12  14752  dvdslelem  14812  odd2np1lem  14845  odd2np1  14846  isprm6  15207  pythagtrip  15320  pc2dvds  15364  mreexexlem4d  16073  mreexexd  16074  mreexexdOLD  16075  irredrmul  18473  mplsubrglem  19203  znidomb  19671  ppttop  20560  filcon  21436  trufil  21463  ufildr  21484  plycj  23751  cosord  23996  logdivlt  24085  isosctrlem2  24263  atans2  24372  wilthlem2  24509  basellem3  24523  lgsdir2lem4  24767  pntpbnd1  24989  mirhl  25289  axcontlem2  25560  axcontlem4  25562  ex-natded5.13-2  26428  hiidge0  27142  chirredlem4  28439  disjxpin  28586  iocinif  28736  erdszelem11  30240  erdsze2lem2  30243  dfon2lem5  30739  trpredrec  30785  nofv  30857  btwnconn1lem14  31180  btwnconn2  31182  poimir  32412  ispridlc  32839  lcvexchlem4  33142  lcvexchlem5  33143  paddss1  33921  paddss2  33922  rexzrexnn0  36186  pell14qrdich  36251  acongsym  36361  dvdsacongtr  36369  or3or  37139  clsk1indlem3  37161  propeqop  40123  nn0eo  42115
  Copyright terms: Public domain W3C validator