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

Theorem orim12d 963
Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 910 for a proof which does not depend on df-an 397. (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 962 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → ((𝜓𝜃) → (𝜒𝜏)))
41, 2, 3syl2anc 584 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 845
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 206  df-an 397  df-or 846
This theorem is referenced by:  orim1d  964  orim2d  965  3orim123d  1444  preq12b  4806  propeqop  5462  fr2nr  5609  sossfld  6136  ordtri3or  6347  ordelinel  6416  funun  6544  soisores  7268  sorpsscmpl  7663  sucexeloniOLD  7737  suceloniOLD  7739  ordunisuc2  7772  fnse  8057  oaord  8486  omord2  8506  omcan  8508  oeord  8527  oecan  8528  nnaord  8558  nnmord  8571  omsmo  8596  swoer  8636  unxpwdom  9483  rankxplim3  9775  cdainflem  10081  ackbij2  10137  sornom  10171  fin23lem20  10231  fpwwe2lem9  10533  inatsk  10672  ltadd2  11217  ltord1  11639  ltmul1  11963  lt2msq  11998  zle0orge1  12474  mul2lt0bi  12975  xmullem2  13138  difreicc  13355  fzospliti  13558  om2uzlti  13809  om2uzlt2i  13810  om2uzf1oi  13812  absor  15139  ruclem12  16077  dvdslelem  16145  odd2np1lem  16176  odd2np1  16177  isprm6  16544  pythagtrip  16660  pc2dvds  16705  mreexexlem4d  17481  mreexexd  17482  ablsimpgprmd  19847  irredrmul  20083  znidomb  20915  mplsubrglem  21356  ppttop  22303  filconn  23180  trufil  23207  ufildr  23228  plycj  25584  cosord  25833  logdivlt  25922  isosctrlem2  26115  atans2  26227  wilthlem2  26364  basellem3  26378  lgsdir2lem4  26622  pntpbnd1  26880  nofv  26951  nolesgn2o  26965  noetalem1  27035  mirhl  27466  axcontlem2  27759  axcontlem4  27761  ex-natded5.13-2  29205  hiidge0  29885  chirredlem4  31180  disjxpin  31351  nn0xmulclb  31518  iocinif  31526  pmtrcnelor  31784  isprmidlc  32058  rhmpreimaprmidl  32062  erdszelem11  33623  erdsze2lem2  33626  satfv1  33785  satfdmlem  33790  fmla1  33809  satffunlem2lem2  33828  dfon2lem5  34194  btwnconn1lem14  34617  btwnconn2  34619  bj-nnford  35148  poimir  36043  ispridlc  36461  lcvexchlem4  37431  lcvexchlem5  37432  paddss1  38212  paddss2  38213  mulgt0con1dlem  40829  rexzrexnn0  41030  pell14qrdich  41095  acongsym  41203  dvdsacongtr  41211  or3or  42200  clsk1indlem3  42220  mnringmulrcld  42413  nn0eo  46509  prelrrx2b  46695  itscnhlc0xyqsol  46746  itschlc0xyqsol  46748  inlinecirc02plem  46767
  Copyright terms: Public domain W3C validator