Theorem jao1i 857

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

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  pm2.64  942  pm2.82  976  sorpssint  7768  preleqg  9684  ltlen  11391  elnnnn0b  12597  znnn0nn  12754  scshwfzeqfzo  14875  nn0enne  16425  dvdsprmpweqnn  16932  dvdsprmpweqle  16933  prmirred  21508  pmatcollpw3fi1  22815  2lgsoddprmlem3  27476  sltlend  27834  prtlem14  38830