Theorem orim12i 538

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	|- ( ph -> ps )
orim12i.2	|- ( ch -> th )

Assertion

Ref	Expression
orim12i	|- ( ( ph \/ ch ) -> ( ps \/ th ) )

Proof of Theorem orim12i

Step	Hyp	Ref	Expression
1		orim12i.1	. . 3 |- ( ph -> ps )
2	1	orcd 407	. 2 |- ( ph -> ( ps \/ th ) )
3		orim12i.2	. . 3 |- ( ch -> th )
4	3	olcd 408	. 2 |- ( ch -> ( ps \/ th ) )
5	2, 4	jaoi 394	1 |- ( ( ph \/ ch ) -> ( ps \/ th ) )

Syntax hints:   -> wi 4   \/ wo 383

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 385

This theorem is referenced by:  orim1i  539  orim2i  540  prlem2  1006  ifpor  1021  eueq3  3381  pwssun  5020  xpima  5576  funcnvuni  7119  2oconcl  7583  fin23lem23  9148  fin23lem19  9158  fin1a2lem13  9234  fin1a2s  9236  nn0ge0  11318  elfzlmr  12582  hash2pwpr  13258  trclfvg  13756  mreexexdOLD  16309  xpcbas  16818  odcl  17955  gexcl  17995  ang180lem4  24542  elim2ifim  29364  locfinref  29908  volmeas  30294  nepss  31599  funpsstri  31663  fvresval  31665  dvasin  33496  dvacos  33497  relexpxpmin  38009  clsk1indlem3  38341  elsprel  41725  resolution  42545