Theorem pm2.61ian 476

Description: Elimination of an antecedent.

Hypotheses

Ref	Expression
pm2.61ian.1	⊢ ((φ ⋀ ψ) → χ)
pm2.61ian.2	⊢ ((¬ φ ⋀ ψ) → χ)

Assertion

Ref	Expression
pm2.61ian	⊢ (ψ → χ)

Proof of Theorem pm2.61ian

Step	Hyp	Ref	Expression
1		pm2.61ian.1	. . 3 ⊢ ((φ ⋀ ψ) → χ)
2	1	ex 373	. 2 ⊢ (φ → (ψ → χ))
3		pm2.61ian.2	. . 3 ⊢ ((¬ φ ⋀ ψ) → χ)
4	3	ex 373	. 2 ⊢ (¬ φ → (ψ → χ))
5	2, 4	pm2.61i 126	1 ⊢ (ψ → χ)

Syntax hints:  ¬ wn 2   → wi 3   ⋀ wa 223

This theorem is referenced by:  4cases 757  sbcom 1256  ax11indalem 1366  ifboth 2371  findsg 3152  tfindsg 3157  funopg 3539  mapsspw 4331  ranklim 4665  climcl 6924  dscmet 7870  unopbdt 9878  nmopco 9966  iintlem1 10512

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain