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  1907  19.40b  1921  19.41v  1982  19.41  2273  2ax6elem  2501  mo3  2591  2mo  2675  relopabi  5807  smoord  8358  fisupg  9262  winalim2  10709  relin01  11766  cshwlen  14874  aalioulem5  26579  musum  27435  chrelat2i  32854  bnj1173  35519  waj-ax  37041  sbn1ALT  37609  hlrelat2  40284  pm11.71  45229  onfrALTlem2  45377  19.41rg  45381  not12an2impnot1  45399  onfrALTlem2VD  45719  2pm13.193VD  45733  ax6e2eqVD  45737  ssfz12  48210