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

Theorem orim12i 909
Description: Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
Hypotheses
Ref Expression
orim12i.1 (𝜑𝜓)
orim12i.2 (𝜒𝜃)
Assertion
Ref Expression
orim12i ((𝜑𝜒) → (𝜓𝜃))

Proof of Theorem orim12i
StepHypRef Expression
1 orim12i.1 . . 3 (𝜑𝜓)
21orcd 874 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 875 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 858 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 848
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 207  df-or 849
This theorem is referenced by:  orim1i  910  orim2i  911  prlem2  1056  ifpor  1073  eueq3  3717  pwssun  5575  xpima  6202  fvresval  7378  0mpo0  7516  funcnvuni  7954  2oconcl  8541  djur  9959  djuun  9966  fin23lem23  10366  fin23lem19  10376  fin1a2lem13  10452  fin1a2s  10454  nn0ge0  12551  elfzlmr  13820  hash2pwpr  14515  trclfvg  15054  xpcbas  18223  odcl  19554  gexcl  19598  ang180lem4  26855  sltn0  27943  n0seo  28405  elim2ifim  32558  locfinref  33840  volmeas  34232  nepss  35718  funpsstri  35766  bj-prmoore  37116  bj-imdirco  37191  dvasin  37711  dvacos  37712  disjorimxrn  38749  relexpxpmin  43730  clsk1indlem3  44056  elsprel  47462  resolution  49318
  Copyright terms: Public domain W3C validator