Theorem prth 555

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 557  mo 1392  2mo 1446  reuss2 2272  ssxp 3252  tfrlem5 3910  cau3ir 6867  cvganz 6876  clm3 7032  climunii 7051  climaddlem3 7069  climmullem8 7080  xplm 7937  xpcn 7938  lmcau 7958  hlimcaui 9061  hlimunii 9063  spanun 9422

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