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

Theorem orim12d 962
Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 909 for a proof which does not depend on df-an 400. (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 961 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → ((𝜓𝜃) → (𝜒𝜏)))
41, 2, 3syl2anc 587 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 844
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 210  df-an 400  df-or 845
This theorem is referenced by:  orim1d  963  orim2d  964  3orim123d  1441  preq12b  4744  propeqop  5365  fr2nr  5501  sossfld  6014  ordtri3or  6195  ordelinel  6261  funun  6374  soisores  7063  sorpsscmpl  7444  suceloni  7512  ordunisuc2  7543  fnse  7814  oaord  8160  omord2  8180  omcan  8182  oeord  8201  oecan  8202  nnaord  8232  nnmord  8245  omsmo  8268  swoer  8306  unxpwdom  9041  rankxplim3  9298  cdainflem  9602  ackbij2  9658  sornom  9692  fin23lem20  9752  fpwwe2lem10  10054  inatsk  10193  ltadd2  10737  ltord1  11159  ltmul1  11483  lt2msq  11518  zle0orge1  11990  mul2lt0bi  12487  xmullem2  12650  difreicc  12866  fzospliti  13068  om2uzlti  13317  om2uzlt2i  13318  om2uzf1oi  13320  absor  14655  ruclem12  15589  dvdslelem  15654  odd2np1lem  15684  odd2np1  15685  isprm6  16051  pythagtrip  16164  pc2dvds  16208  mreexexlem4d  16913  mreexexd  16914  ablsimpgprmd  19233  irredrmul  19456  znidomb  20256  mplsubrglem  20680  ppttop  21615  filconn  22491  trufil  22518  ufildr  22539  plycj  24877  cosord  25126  logdivlt  25215  isosctrlem2  25408  atans2  25520  wilthlem2  25657  basellem3  25671  lgsdir2lem4  25915  pntpbnd1  26173  mirhl  26476  axcontlem2  26762  axcontlem4  26764  ex-natded5.13-2  28204  hiidge0  28884  chirredlem4  30179  disjxpin  30354  nn0xmulclb  30525  iocinif  30533  pmtrcnelor  30788  isprmidlc  31031  rhmpreimaprmidl  31035  erdszelem11  32556  erdsze2lem2  32559  satfv1  32718  satfdmlem  32723  fmla1  32742  satffunlem2lem2  32761  dfon2lem5  33140  trpredrec  33185  nofv  33272  nolesgn2o  33286  btwnconn1lem14  33669  btwnconn2  33671  bj-nnford  34190  poimir  35083  ispridlc  35501  lcvexchlem4  36326  lcvexchlem5  36327  paddss1  37106  paddss2  37107  mulgt0con1dlem  39569  rexzrexnn0  39732  pell14qrdich  39797  acongsym  39904  dvdsacongtr  39912  or3or  40711  clsk1indlem3  40733  mnringmulrcld  40923  nn0eo  44929  prelrrx2b  45115  itscnhlc0xyqsol  45166  itschlc0xyqsol  45168  inlinecirc02plem  45187
  Copyright terms: Public domain W3C validator