Theorem jao1i 872

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm2.64  956  pm2.82  991  imadifssranOLD  6202  imadifssranOLDOLD  6203  sorpssint  7749  preleqg  9616  ltlen  11411  elnnnn0b  12650  znnn0nn  12810  scshwfzeqfzo  14977  nn0enne  16547  dvdsprmpweqnn  17063  dvdsprmpweqle  17064  prmirred  21780  pmatcollpw3fi1  23106  2lgsoddprmlem3  27741  ltlesnd  28132  prtlem14  39931