Theorem orim12i 748

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

Step	Hyp	Ref	Expression
1		orim12i.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	orcd 722	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃))
3		orim12i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	olcd 723	. 2 ⊢ (𝜒 → (𝜓 ∨ 𝜃))
5	2, 4	jaoi 705	1 ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1i  749  orim2i  750  dcim  826  pm5.12dc  895  pm5.14dc  896  pm5.55dc  898  pm5.54dc  903  prlem2  958  xordc1  1371  19.43  1607  eueq3dc  2858  inssun  3316  abvor0dc  3386  ifmdc  3509  undifexmid  4117  pwssunim  4206  ordtriexmid  4437  ordtri2orexmid  4438  ontr2exmid  4440  onsucsssucexmid  4442  onsucelsucexmid  4445  ordsoexmid  4477  0elsucexmid  4480  ordpwsucexmid  4485  ordtri2or2exmid  4486  funcnvuni  5192  oprabidlem  5802  2oconcl  6336  inffiexmid  6800  unfiexmid  6806  ctssexmid  7024  exmidonfinlem  7049  sup3exmid  8715  zeo  9156  ef0lem  11366