Theorem pm3.21 477

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 23	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜑))
2	1	expcom 419	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  iba  537  ancr  556  anc2r  564  19.29r  1906  19.40b  1920  19.41v  1981  19.41  2271  2ax6elem  2499  mo3  2589  2mo  2673  relopabi  5799  smoord  8376  fisupg  9282  winalim2  10784  relin01  11843  cshwlen  14954  aalioulem5  26668  musum  27523  chrelat2i  32972  bnj1173  35678  waj-ax  37294  sbn1ALT  37862  hlrelat2  40553  pm11.71  45474  onfrALTlem2  45622  19.41rg  45626  not12an2impnot1  45644  onfrALTlem2VD  45964  2pm13.193VD  45978  ax6e2eqVD  45982  ssfz12  48477