Theorem orim12i 363

Description: Disjoin antecedents and consequents of two premises.

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	. . . . 5 |- (ph -> ps)
2	1	con3i 114	. . . 4 |- (-. ps -> -. ph)
3		orim12i.2	. . . . 5 |- (ch -> th)
4	3	con3i 114	. . . 4 |- (-. th -> -. ch)
5	2, 4	anim12i 360	. . 3 |- ((-. ps /\ -. th) -> (-. ph /\ -. ch))
6	5	con3i 114	. 2 |- (-. (-. ph /\ -. ch) -> -. (-. ps /\ -. th))
7		oran 338	. 2 |- ((ph \/ ch) <-> -. (-. ph /\ -. ch))
8		oran 338	. 2 |- ((ps \/ th) <-> -. (-. ps /\ -. th))
9	6, 7, 8	3imtr4i 236	1 |- ((ph \/ ch) -> (ps \/ th))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239   /\ wa 240

This theorem is referenced by:  orim1i 364  orim2i 365  iforOLD 3009  pwssun 3578  dfco2aOLD 4395  funcnvuni 4482  ltadd2i 6765  ltmul1ii 6999  efltbi 8672  sinperlem2 10036  cosh111lem2 10069  nepss 13820  funpsstri 13835  fvresval 13841  condis 14269  condisd 14270  fprod1ib 14686  prfOLD 15680

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242

Copyright terms: Public domain