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

This theorem is referenced by:  pm2.64  940  pm2.82  974  sorpssint  7738  preleqg  9639  ltlen  11346  elnnnn0b  12547  znnn0nn  12704  scshwfzeqfzo  14810  nn0enne  16354  dvdsprmpweqnn  16854  dvdsprmpweqle  16855  prmirred  21400  pmatcollpw3fi1  22703  2lgsoddprmlem3  27360  sltlend  27717  prtlem14  38346

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »