Theorem jao1i 869

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 868	1 ⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑))

Syntax hints:   → wi 4   ∨ wo 858

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 859

This theorem is referenced by:  pm2.64  954  pm2.82  989  imadifssran  6136  sorpssint  7716  preleqg  9570  ltlen  11284  elnnnn0b  12525  znnn0nn  12684  scshwfzeqfzo  14839  nn0enne  16411  dvdsprmpweqnn  16921  dvdsprmpweqle  16922  prmirred  21526  pmatcollpw3fi1  22848  2lgsoddprmlem3  27478  ltlesnd  27839  prtlem14  39498