Theorem orim12da 980

Description: Deduce a disjunction from another one. Variation on orim12d 979. (Contributed by Thierry Arnoux, 18-May-2025.)

Hypotheses

Ref	Expression
orim12da.1	⊢ ((𝜑 ∧ 𝜓) → 𝜃)
orim12da.2	⊢ ((𝜑 ∧ 𝜒) → 𝜏)
orim12da.3	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Assertion

Ref	Expression
orim12da	⊢ (𝜑 → (𝜃 ∨ 𝜏))

Proof of Theorem orim12da

Step	Hyp	Ref	Expression
1		orim12da.3	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
2		orim12da.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
3	2	ex 418	. . 3 ⊢ (𝜑 → (𝜓 → 𝜃))
4		orim12da.2	. . . 4 ⊢ ((𝜑 ∧ 𝜒) → 𝜏)
5	4	ex 418	. . 3 ⊢ (𝜑 → (𝜒 → 𝜏))
6	3, 5	orim12d 979	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜒) → (𝜃 ∨ 𝜏)))
7	1, 6	mpd 16	1 ⊢ (𝜑 → (𝜃 ∨ 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  lnincplng  29244  plngmiropp  29254  prlngsym  29401  ricdomn1  33832  drngmxidlr  33984  drnglring  34006  dflring2  34007  dflringlem2  34009  dflring3  34011  rsprprmprmidl  34036  rsprprmprmidlb  34037  rprmirredb  34046  rprmdvdsprod  34048  mplidomlem  34141  rtelextdg2  34341  squeezedltsq  47856