Theorem orim12i 271

Description: Conjoin antecedents and consequents of two premises.

Hypotheses

Ref	Expression
orim12i.1	⊢ (φ → ψ)
orim12i.2	⊢ (χ → θ)

Assertion

Ref	Expression
orim12i	⊢ ((φ ∨ χ) → (ψ ∨ θ))

Proof of Theorem orim12i

Step	Hyp	Ref	Expression
1		orim12i.1	. . . . 5 ⊢ (φ → ψ)
2	1	con3i 90	. . . 4 ⊢ (¬ ψ → ¬ φ)
3		orim12i.2	. . . . 5 ⊢ (χ → θ)
4	3	con3i 90	. . . 4 ⊢ (¬ θ → ¬ χ)
5	2, 4	anim12i 268	. . 3 ⊢ ((¬ ψ ∧ ¬ θ) → (¬ φ ∧ ¬ χ))
6	5	con3i 90	. 2 ⊢ (¬ (¬ φ ∧ ¬ χ) → ¬ (¬ ψ ∧ ¬ θ))
7		oran 255	. 2 ⊢ ((φ ∨ χ) ↔ ¬ (¬ φ ∧ ¬ χ))
8		oran 255	. 2 ⊢ ((ψ ∨ θ) ↔ ¬ (¬ ψ ∧ ¬ θ))
9	6, 7, 8	3imtr4 192	1 ⊢ ((φ ∨ χ) → (ψ ∨ θ))

Syntax hints:  ¬ wn 1   → wi 2   ∨ wo 195   ∧ wa 196

This theorem is referenced by:  orim1i 272  orim2i 273  pwssun 1917  funcnvuni 2706  nn0ge0i 4559  absor 4853

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

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org