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  6197  imadifssranOLD  6198  sorpssint  7735  preleqg  9597  ltlen  11338  elnnnn0b  12575  znnn0nn  12735  scshwfzeqfzo  14900  nn0enne  16470  dvdsprmpweqnn  16980  dvdsprmpweqle  16981  prmirred  21690  pmatcollpw3fi1  23016  2lgsoddprmlem3  27653  ltlesnd  28014  prtlem14  39750