Theorem jao1i 858

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  pm2.64  943  pm2.82  977  imadifssran  6124  sorpssint  7709  preleqg  9568  ltlen  11275  elnnnn0b  12486  znnn0nn  12645  scshwfzeqfzo  14792  nn0enne  16347  dvdsprmpweqnn  16856  dvdsprmpweqle  16857  prmirred  21384  pmatcollpw3fi1  22675  2lgsoddprmlem3  27325  sltlend  27683  prtlem14  38867