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

Theorem orim12d 958
Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 905 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 957 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → ((𝜓𝜃) → (𝜒𝜏)))
41, 2, 3syl2anc 584 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 841
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 208  df-an 397  df-or 842
This theorem is referenced by:  orim1d  959  orim2d  960  3orim123d  1435  preq12b  4775  propeqop  5389  fr2nr  5527  sossfld  6037  ordtri3or  6217  ordelinel  6283  funun  6394  soisores  7069  sorpsscmpl  7449  suceloni  7516  ordunisuc2  7547  fnse  7818  oaord  8163  omord2  8183  omcan  8185  oeord  8204  oecan  8205  nnaord  8235  nnmord  8248  omsmo  8271  swoer  8309  unxpwdom  9042  rankxplim3  9299  cdainflem  9602  ackbij2  9654  sornom  9688  fin23lem20  9748  fpwwe2lem10  10050  inatsk  10189  ltadd2  10733  ltord1  11155  ltmul1  11479  lt2msq  11514  zle0orge1  11987  mul2lt0bi  12485  xmullem2  12648  difreicc  12860  fzospliti  13059  om2uzlti  13308  om2uzlt2i  13309  om2uzf1oi  13311  absor  14650  ruclem12  15584  dvdslelem  15649  odd2np1lem  15679  odd2np1  15680  isprm6  16048  pythagtrip  16161  pc2dvds  16205  mreexexlem4d  16908  mreexexd  16909  ablsimpgprmd  19168  irredrmul  19388  mplsubrglem  20149  znidomb  20638  ppttop  21545  filconn  22421  trufil  22448  ufildr  22469  plycj  24796  cosord  25043  logdivlt  25131  isosctrlem2  25324  atans2  25436  wilthlem2  25574  basellem3  25588  lgsdir2lem4  25832  pntpbnd1  26090  mirhl  26393  axcontlem2  26679  axcontlem4  26681  ex-natded5.13-2  28123  hiidge0  28803  chirredlem4  30098  disjxpin  30267  nn0xmulclb  30423  iocinif  30431  pmtrcnelor  30663  isprmidlc  30882  erdszelem11  32346  erdsze2lem2  32349  satfv1  32508  satfdmlem  32513  fmla1  32532  satffunlem2lem2  32551  dfon2lem5  32930  trpredrec  32975  nofv  33062  nolesgn2o  33076  btwnconn1lem14  33459  btwnconn2  33461  bj-nnford  33978  poimir  34807  ispridlc  35231  lcvexchlem4  36055  lcvexchlem5  36056  paddss1  36835  paddss2  36836  rexzrexnn0  39281  pell14qrdich  39346  acongsym  39453  dvdsacongtr  39461  or3or  40251  clsk1indlem3  40273  nn0eo  44486  prelrrx2b  44599  itscnhlc0xyqsol  44650  itschlc0xyqsol  44652  inlinecirc02plem  44671
  Copyright terms: Public domain W3C validator