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

Theorem orim12i 537
 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 406 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 407 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 393 1 ((𝜑𝜒) → (𝜓𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382 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 196  df-or 384 This theorem is referenced by:  orim1i  538  orim2i  539  prlem2  998  ifpor  1015  eueq3  3348  pwssun  4944  xpima  5495  funcnvuni  7012  2oconcl  7470  fin23lem23  9031  fin23lem19  9041  fin1a2lem13  9117  fin1a2s  9119  nn0ge0  11195  hash2pwpr  13115  trclfvg  13604  mreexexdOLD  16132  xpcbas  16641  odcl  17778  gexcl  17818  ang180lem4  24342  cusgrares  26001  2pthlem2  26126  elim2ifim  28748  locfinref  29236  volmeas  29621  nepss  30854  funpsstri  30909  fvresval  30911  dvasin  32666  dvacos  32667  relexpxpmin  37028  clsk1indlem3  37361  elfzlmr  40366  resolution  42354
 Copyright terms: Public domain W3C validator