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

Theorem orim12i 906
 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 870 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 871 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 854 1 ((𝜑𝜒) → (𝜓𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 844 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 845 This theorem is referenced by:  orim1i  907  orim2i  908  prlem2  1051  ifpor  1068  eueq3  3650  pwssun  5422  xpima  6007  0mpo0  7217  funcnvuni  7621  2oconcl  8114  djur  9335  djuun  9342  fin23lem23  9740  fin23lem19  9750  fin1a2lem13  9826  fin1a2s  9828  nn0ge0  11913  elfzlmr  13149  hash2pwpr  13833  trclfvg  14369  xpcbas  17423  odcl  18660  gexcl  18701  ang180lem4  25408  elim2ifim  30322  locfinref  31209  volmeas  31615  nepss  33076  funpsstri  33136  fvresval  33138  bj-prmoore  34549  bj-imdirco  34624  dvasin  35160  dvacos  35161  disjorimxrn  36157  relexpxpmin  40461  clsk1indlem3  40789  elsprel  44035  resolution  45368
 Copyright terms: Public domain W3C validator