Theorem jao1i 865

Description: Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.)

Hypothesis

Ref	Expression
jao1i.1	⊢ (𝜓 → (𝜒 → 𝜑))

Assertion

Ref	Expression
jao1i	⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑))

Proof of Theorem jao1i

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 ⊢ (𝜑 → (𝜒 → 𝜑))
2		jao1i.1	. 2 ⊢ (𝜓 → (𝜒 → 𝜑))
3	1, 2	jaoi 864	1 ⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑))

Syntax hints:   → wi 4   ∨ wo 854

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

This theorem depends on definitions:  df-bi 209  df-or 855

This theorem is referenced by:  pm2.64  950  pm2.82  984  imadifssran  6105  sorpssint  7679  preleqg  9531  ltlen  11243  elnnnn0b  12476  znnn0nn  12635  scshwfzeqfzo  14783  nn0enne  16341  dvdsprmpweqnn  16851  dvdsprmpweqle  16852  prmirred  21452  pmatcollpw3fi1  22774  2lgsoddprmlem3  27398  ltlesnd  27759  prtlem14  39379