Theorem pm3.21 474

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 416	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  iba  530  ancr  549  anc2r  557  19.29r  1871  19.40b  1885  19.41v  1946  19.41  2233  2ax6elem  2489  mo3  2644  2mo  2729  relopabi  5688  smoord  7996  fisupg  8760  winalim2  10112  relin01  11158  cshwlen  14155  aalioulem5  24919  musum  25762  chrelat2i  30136  bnj1173  32269  waj-ax  33757  hlrelat2  36533  pm11.71  40722  onfrALTlem2  40873  19.41rg  40877  not12an2impnot1  40895  onfrALTlem2VD  41216  2pm13.193VD  41230  ax6e2eqVD  41234  ssfz12  43508