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 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 961 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → ((𝜓𝜃) → (𝜒𝜏)))
41, 2, 3syl2anc 584 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 206  df-an 397  df-or 845
This theorem is referenced by:  orim1d  963  orim2d  964  3orim123d  1443  preq12b  4782  propeqop  5422  fr2nr  5568  sossfld  6094  ordtri3or  6302  ordelinel  6368  funun  6487  soisores  7207  sorpsscmpl  7596  sucexeloni  7667  suceloniOLD  7669  ordunisuc2  7700  fnse  7983  oaord  8387  omord2  8407  omcan  8409  oeord  8428  oecan  8429  nnaord  8459  nnmord  8472  omsmo  8497  swoer  8537  unxpwdom  9357  rankxplim3  9648  cdainflem  9952  ackbij2  10008  sornom  10042  fin23lem20  10102  fpwwe2lem9  10404  inatsk  10543  ltadd2  11088  ltord1  11510  ltmul1  11834  lt2msq  11869  zle0orge1  12345  mul2lt0bi  12845  xmullem2  13008  difreicc  13225  fzospliti  13428  om2uzlti  13679  om2uzlt2i  13680  om2uzf1oi  13682  absor  15021  ruclem12  15959  dvdslelem  16027  odd2np1lem  16058  odd2np1  16059  isprm6  16428  pythagtrip  16544  pc2dvds  16589  mreexexlem4d  17365  mreexexd  17366  ablsimpgprmd  19727  irredrmul  19958  znidomb  20778  mplsubrglem  21219  ppttop  22166  filconn  23043  trufil  23070  ufildr  23091  plycj  25447  cosord  25696  logdivlt  25785  isosctrlem2  25978  atans2  26090  wilthlem2  26227  basellem3  26241  lgsdir2lem4  26485  pntpbnd1  26743  mirhl  27049  axcontlem2  27342  axcontlem4  27344  ex-natded5.13-2  28789  hiidge0  29469  chirredlem4  30764  disjxpin  30936  nn0xmulclb  31103  iocinif  31111  pmtrcnelor  31369  isprmidlc  31632  rhmpreimaprmidl  31636  erdszelem11  33172  erdsze2lem2  33175  satfv1  33334  satfdmlem  33339  fmla1  33358  satffunlem2lem2  33377  dfon2lem5  33772  nofv  33869  nolesgn2o  33883  noetalem1  33953  btwnconn1lem14  34411  btwnconn2  34413  bj-nnford  34942  poimir  35819  ispridlc  36237  lcvexchlem4  37058  lcvexchlem5  37059  paddss1  37838  paddss2  37839  mulgt0con1dlem  40434  rexzrexnn0  40633  pell14qrdich  40698  acongsym  40805  dvdsacongtr  40813  or3or  41638  clsk1indlem3  41660  mnringmulrcld  41853  nn0eo  45885  prelrrx2b  46071  itscnhlc0xyqsol  46122  itschlc0xyqsol  46124  inlinecirc02plem  46143
  Copyright terms: Public domain W3C validator