Theorem jao1i 871

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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  pm2.64  956  pm2.82  991  imadifssran  6203  imadifssranOLD  6204  sorpssint  7731  preleqg  9584  ltlen  11311  elnnnn0b  12548  znnn0nn  12707  scshwfzeqfzo  14863  nn0enne  16435  dvdsprmpweqnn  16945  dvdsprmpweqle  16946  prmirred  21593  pmatcollpw3fi1  22914  2lgsoddprmlem3  27544  ltlesnd  27905  prtlem14  39572