Theorem jao1i 856

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

Syntax hints:   → wi 4   ∨ wo 845

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 206  df-or 846

This theorem is referenced by:  pm2.64  939  pm2.82  973  sorpssint  7734  preleqg  9649  ltlen  11354  elnnnn0b  12560  znnn0nn  12717  scshwfzeqfzo  14828  nn0enne  16372  dvdsprmpweqnn  16880  dvdsprmpweqle  16881  prmirred  21458  pmatcollpw3fi1  22776  2lgsoddprmlem3  27438  sltlend  27796  prtlem14  38583