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  6104  sorpssint  7673  preleqg  9530  ltlen  11236  elnnnn0b  12447  znnn0nn  12606  scshwfzeqfzo  14752  nn0enne  16307  dvdsprmpweqnn  16816  dvdsprmpweqle  16817  prmirred  21400  pmatcollpw3fi1  22692  2lgsoddprmlem3  27342  sltlend  27700  prtlem14  38872