MPE Home 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 197  df-or 384
This theorem is referenced by:  orim1i  538  orim2i  539  prlem2  1026  ifpor  1041  eueq3  3414  pwssun  5049  xpima  5611  funcnvuni  7161  2oconcl  7628  fin23lem23  9186  fin23lem19  9196  fin1a2lem13  9272  fin1a2s  9274  nn0ge0  11356  elfzlmr  12622  hash2pwpr  13296  trclfvg  13800  mreexexdOLD  16356  xpcbas  16865  odcl  18001  gexcl  18041  ang180lem4  24587  elim2ifim  29490  locfinref  30036  volmeas  30422  nepss  31725  funpsstri  31789  fvresval  31791  dvasin  33626  dvacos  33627  relexpxpmin  38326  clsk1indlem3  38658  elsprel  42050  resolution  42873
  Copyright terms: Public domain W3C validator