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 873 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 874 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 857 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847
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 210  df-or 848
This theorem is referenced by:  orim1i  910  orim2i  911  prlem2  1056  ifpor  1073  eueq3  3624  pwssun  5451  xpima  6045  0mpo0  7294  funcnvuni  7709  2oconcl  8230  djur  9535  djuun  9542  fin23lem23  9940  fin23lem19  9950  fin1a2lem13  10026  fin1a2s  10028  nn0ge0  12115  elfzlmr  13356  hash2pwpr  14042  trclfvg  14578  xpcbas  17685  odcl  18928  gexcl  18969  ang180lem4  25695  elim2ifim  30607  locfinref  31505  volmeas  31911  nepss  33377  funpsstri  33458  fvresval  33460  sltn0  33822  bj-prmoore  35021  bj-imdirco  35096  dvasin  35598  dvacos  35599  disjorimxrn  36593  relexpxpmin  41002  clsk1indlem3  41330  elsprel  44600  resolution  46174
  Copyright terms: Public domain W3C validator