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

Theorem orim12i 902
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 869 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 870 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 851 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 841
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 208  df-or 842
This theorem is referenced by:  orim1i  903  orim2i  904  prlem2  1047  ifpor  1063  eueq3  3699  pwssun  5448  xpima  6032  0mpo0  7226  funcnvuni  7625  2oconcl  8117  djur  9336  djuun  9343  fin23lem23  9736  fin23lem19  9746  fin1a2lem13  9822  fin1a2s  9824  nn0ge0  11910  elfzlmr  13139  hash2pwpr  13822  trclfvg  14363  xpcbas  17416  odcl  18593  gexcl  18634  ang180lem4  25317  elim2ifim  30227  locfinref  31004  volmeas  31389  nepss  32845  funpsstri  32905  fvresval  32907  dvasin  34859  dvacos  34860  disjorimxrn  35858  relexpxpmin  39940  clsk1indlem3  40271  elsprel  43514  resolution  44828
  Copyright terms: Public domain W3C validator