Theorem jao1i 859

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

Syntax hints:   → wi 4   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  pm2.64  944  pm2.82  978  imadifssran  6110  sorpssint  7681  preleqg  9530  ltlen  11241  elnnnn0b  12475  znnn0nn  12634  scshwfzeqfzo  14782  nn0enne  16340  dvdsprmpweqnn  16850  dvdsprmpweqle  16851  prmirred  21467  pmatcollpw3fi1  22766  2lgsoddprmlem3  27394  ltlesnd  27756  prtlem14  39337