Theorem prth 554

Description: Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it 'praeclarum theorema.'

Assertion

Ref	Expression
prth	⊢ (((φ → ψ) ⋀ (χ → θ)) → ((φ ⋀ χ) → (ψ ⋀ θ)))

Proof of Theorem prth

Step	Hyp	Ref	Expression
1		pm3.2 283	. . . . 5 ⊢ (ψ → (θ → (ψ ⋀ θ)))
2	1	imim2d 25	. . . 4 ⊢ (ψ → ((χ → θ) → (χ → (ψ ⋀ θ))))
3	2	imim2i 17	. . 3 ⊢ ((φ → ψ) → (φ → ((χ → θ) → (χ → (ψ ⋀ θ)))))
4	3	com23 32	. 2 ⊢ ((φ → ψ) → ((χ → θ) → (φ → (χ → (ψ ⋀ θ)))))
5	4	imp4b 365	1 ⊢ (((φ → ψ) ⋀ (χ → θ)) → ((φ ⋀ χ) → (ψ ⋀ θ)))

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  anim12d 556  mo 1386  2mo 1440  reuss2 2265  ssxp 3246  tfrlem5 3900  cau3ir 6852  cvganz 6861  clm3 7017  climunii 7035  climaddlem3 7052  climmullem8 7063  xplm 7909  xpcn 7910  lmcau 7930  hlimcaui 9027  hlimunii 9029  spanun 9382

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