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

Theorem orim12d 882
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 877 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → ((𝜓𝜃) → (𝜒𝜏)))
41, 2, 3syl2anc 692 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383
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 197  df-or 385  df-an 386
This theorem is referenced by:  orim1d  883  orim2d  884  3orim123d  1404  preq12b  4357  prel12  4358  propeqop  4940  fr2nr  5062  sossfld  5549  ordtri3or  5724  ordelinel  5794  funun  5900  soisores  6542  sorpsscmpl  6913  suceloni  6975  ordunisuc2  7006  fnse  7254  oaord  7587  omord2  7607  omcan  7609  oeord  7628  oecan  7629  nnaord  7659  nnmord  7672  omsmo  7694  swoer  7732  unxpwdom  8454  rankxplim3  8704  cdainflem  8973  ackbij2  9025  sornom  9059  fin23lem20  9119  fpwwe2lem10  9421  inatsk  9560  ltadd2  10101  ltord1  10514  ltmul1  10833  lt2msq  10868  mul2lt0bi  11896  xmullem2  12054  difreicc  12262  fzospliti  12457  om2uzlti  12705  om2uzlt2i  12706  om2uzf1oi  12708  absor  13990  ruclem12  14914  dvdslelem  14974  odd2np1lem  15007  odd2np1  15008  isprm6  15369  pythagtrip  15482  pc2dvds  15526  mreexexlem4d  16247  mreexexd  16248  mreexexdOLD  16249  irredrmul  18647  mplsubrglem  19379  znidomb  19850  ppttop  20751  filconn  21627  trufil  21654  ufildr  21675  plycj  23971  cosord  24216  logdivlt  24305  isosctrlem2  24483  atans2  24592  wilthlem2  24729  basellem3  24743  lgsdir2lem4  24987  pntpbnd1  25209  mirhl  25508  axcontlem2  25779  axcontlem4  25781  ex-natded5.13-2  27161  hiidge0  27843  chirredlem4  29140  disjxpin  29287  iocinif  29428  erdszelem11  30944  erdsze2lem2  30947  dfon2lem5  31446  trpredrec  31492  nofv  31564  btwnconn1lem14  31902  btwnconn2  31904  poimir  33113  ispridlc  33540  lcvexchlem4  33843  lcvexchlem5  33844  paddss1  34622  paddss2  34623  rexzrexnn0  36887  pell14qrdich  36952  acongsym  37062  dvdsacongtr  37070  or3or  37840  clsk1indlem3  37862  nn0eo  41640
  Copyright terms: Public domain W3C validator