Theorem jao1i 864

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

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  pm2.64  949  pm2.82  983  imadifssran  6102  sorpssint  7676  preleqg  9527  ltlen  11238  elnnnn0b  12472  znnn0nn  12631  scshwfzeqfzo  14779  nn0enne  16337  dvdsprmpweqnn  16847  dvdsprmpweqle  16848  prmirred  21449  pmatcollpw3fi1  22771  2lgsoddprmlem3  27395  ltlesnd  27757  prtlem14  39366