Theorem orim12i 336

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 98	. . . 4 |- (-. ps -> -. ph)
3		orim12i.2	. . . . 5 |- (ch -> th)
4	3	con3i 98	. . . 4 |- (-. th -> -. ch)
5	2, 4	anim12i 333	. . 3 |- ((-. ps /\ -. th) -> (-. ph /\ -. ch))
6	5	con3i 98	. 2 |- (-. (-. ph /\ -. ch) -> -. (-. ps /\ -. th))
7		oran 312	. 2 |- ((ph \/ ch) <-> -. (-. ph /\ -. ch))
8		oran 312	. 2 |- ((ps \/ th) <-> -. (-. ps /\ -. th))
9	6, 7, 8	3imtr4 219	1 |- ((ph \/ ch) -> (ps \/ th))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222   /\ wa 223

This theorem is referenced by:  orim1i 337  orim2i 338  ifor 2377  pwssun 2822  funcnvuni 3556  ltadd2 5572  ltmul1i 5785  efltb 7356  sinperlem2 8625  cosh111lem2 8649

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 147  df-or 224  df-an 225

Copyright terms: Public domain