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  6209  imadifssranOLDOLD  6210  sorpssint  7759  preleqg  9629  ltlen  11424  elnnnn0b  12663  znnn0nn  12823  scshwfzeqfzo  14991  nn0enne  16562  dvdsprmpweqnn  17078  dvdsprmpweqle  17079  prmirred  21795  pmatcollpw3fi1  23121  2lgsoddprmlem3  27756  ltlesnd  28147  prtlem14  40074