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

Theorem orim12i 536
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 405 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 406 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 392 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381
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 195  df-or 383
This theorem is referenced by:  orim1i  537  orim2i  538  prlem2  997  ifpor  1014  eueq3  3347  pwssun  4934  xpima  5481  funcnvuni  6989  2oconcl  7447  fin23lem23  9008  fin23lem19  9018  fin1a2lem13  9094  fin1a2s  9096  nn0ge0  11165  hash2pwpr  13065  trclfvg  13550  mreexexdOLD  16078  xpcbas  16587  odcl  17724  gexcl  17764  ang180lem4  24259  cusgrares  25767  2pthlem2  25892  elim2ifim  28554  locfinref  29042  volmeas  29427  nepss  30660  funpsstri  30715  fvresval  30717  dvasin  32462  dvacos  32463  relexpxpmin  36824  clsk1indlem3  37157  elfzlmr  40186  resolution  42310
  Copyright terms: Public domain W3C validator