Theorem jao1i 871

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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  pm2.64  956  pm2.82  991  imadifssran  6202  imadifssranOLD  6203  sorpssint  7730  preleqg  9580  ltlen  11306  elnnnn0b  12543  znnn0nn  12702  scshwfzeqfzo  14859  nn0enne  16430  dvdsprmpweqnn  16940  dvdsprmpweqle  16941  prmirred  21624  pmatcollpw3fi1  22945  2lgsoddprmlem3  27578  ltlesnd  27939  prtlem14  39668