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  imadifssran  6204  imadifssranOLD  6205  sorpssint  7740  preleqg  9591  ltlen  11328  elnnnn0b  12565  znnn0nn  12725  scshwfzeqfzo  14889  nn0enne  16459  dvdsprmpweqnn  16969  dvdsprmpweqle  16970  prmirred  21676  pmatcollpw3fi1  22997  2lgsoddprmlem3  27631  ltlesnd  27992  prtlem14  39708