Theorem orim12i 343

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 104	. . . 4 |- (-. ps -> -. ph)
3		orim12i.2	. . . . 5 |- (ch -> th)
4	3	con3i 104	. . . 4 |- (-. th -> -. ch)
5	2, 4	anim12i 340	. . 3 |- ((-. ps /\ -. th) -> (-. ph /\ -. ch))
6	5	con3i 104	. 2 |- (-. (-. ph /\ -. ch) -> -. (-. ps /\ -. th))
7		oran 319	. 2 |- ((ph \/ ch) <-> -. (-. ph /\ -. ch))
8		oran 319	. 2 |- ((ps \/ th) <-> -. (-. ps /\ -. th))
9	6, 7, 8	3imtr4i 226	1 |- ((ph \/ ch) -> (ps \/ th))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 229   /\ wa 230

This theorem is referenced by:  orim1i 344  orim2i 345  ifor 2433  pwssun 2883  funcnvuni 3621  ltadd2i 5655  ltmul1ii 5879  efltbi 7498  sinperlem2 8770  cosh111lem2 8798

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 154  df-or 231  df-an 232

Copyright terms: Public domain