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  29149  plngmiropp  29159  prlngsym  29306  ricdomn1  33737  drngmxidlr  33888  drnglring  33910  dflring2  33911  dflringlem2  33913  dflring3  33915  rsprprmprmidl  33940  rsprprmprmidlb  33941  rprmirredb  33950  rprmdvdsprod  33952  mplidomlem  34045  rtelextdg2  34245  squeezedltsq  47738