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

Theorem orim12d 964
Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 911 for a proof which does not depend on df-an 398. (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 963 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → ((𝜓𝜃) → (𝜒𝜏)))
41, 2, 3syl2anc 585 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846
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 398  df-or 847
This theorem is referenced by:  orim1d  965  orim2d  966  3orim123d  1445  preq12b  4813  propeqop  5469  fr2nr  5616  sossfld  6143  ordtri3or  6354  ordelinel  6423  funun  6552  soisores  7277  sorpsscmpl  7676  sucexeloniOLD  7750  suceloniOLD  7752  ordunisuc2  7785  fnse  8070  oaord  8499  omord2  8519  omcan  8521  oeord  8540  oecan  8541  nnaord  8571  nnmord  8584  omsmo  8609  swoer  8685  unxpwdom  9532  rankxplim3  9824  cdainflem  10130  ackbij2  10186  sornom  10220  fin23lem20  10280  fpwwe2lem9  10582  inatsk  10721  ltadd2  11266  ltord1  11688  ltmul1  12012  lt2msq  12047  zle0orge1  12523  mul2lt0bi  13028  xmullem2  13191  difreicc  13408  fzospliti  13611  om2uzlti  13862  om2uzlt2i  13863  om2uzf1oi  13865  absor  15192  ruclem12  16130  dvdslelem  16198  odd2np1lem  16229  odd2np1  16230  isprm6  16597  pythagtrip  16713  pc2dvds  16758  mreexexlem4d  17534  mreexexd  17535  ablsimpgprmd  19901  irredrmul  20145  lringuplu  20198  znidomb  20984  mplsubrglem  21426  ppttop  22373  filconn  23250  trufil  23277  ufildr  23298  plycj  25654  cosord  25903  logdivlt  25992  isosctrlem2  26185  atans2  26297  wilthlem2  26434  basellem3  26448  lgsdir2lem4  26692  pntpbnd1  26950  nofv  27021  nolesgn2o  27035  noetalem1  27105  mirhl  27663  axcontlem2  27956  axcontlem4  27958  ex-natded5.13-2  29402  hiidge0  30082  chirredlem4  31377  disjxpin  31548  nn0xmulclb  31718  iocinif  31726  pmtrcnelor  31984  isprmidlc  32260  rhmpreimaprmidl  32264  erdszelem11  33835  erdsze2lem2  33838  satfv1  33997  satfdmlem  34002  fmla1  34021  satffunlem2lem2  34040  dfon2lem5  34401  btwnconn1lem14  34714  btwnconn2  34716  bj-nnford  35245  poimir  36140  ispridlc  36558  lcvexchlem4  37528  lcvexchlem5  37529  paddss1  38309  paddss2  38310  mulgt0con1dlem  40955  rexzrexnn0  41156  pell14qrdich  41221  acongsym  41329  dvdsacongtr  41337  or3or  42369  clsk1indlem3  42389  mnringmulrcld  42582  nn0eo  46688  prelrrx2b  46874  itscnhlc0xyqsol  46925  itschlc0xyqsol  46927  inlinecirc02plem  46946
  Copyright terms: Public domain W3C validator