Theorem pm3.21 475

Description: Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
pm3.21	⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))

Proof of Theorem pm3.21

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜑))
2	1	expcom 417	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  iba  535  ancr  554  anc2r  562  19.29r  1893  19.40b  1907  19.41v  1968  19.41  2269  2ax6elem  2500  mo3  2590  2mo  2674  relopabi  5793  smoord  8331  fisupg  9228  winalim2  10651  relin01  11708  cshwlen  14809  aalioulem5  26377  musum  27232  chrelat2i  32514  bnj1173  35261  waj-ax  36738  sbn1ALT  37307  hlrelat2  39991  pm11.71  44937  onfrALTlem2  45086  19.41rg  45090  not12an2impnot1  45108  onfrALTlem2VD  45428  2pm13.193VD  45442  ax6e2eqVD  45446  ssfz12  47872