Theorem pm3.21 476

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  iba  536  ancr  555  anc2r  563  19.29r  1904  19.40b  1918  19.41v  1979  19.41  2271  2ax6elem  2502  mo3  2592  2mo  2676  relopabi  5811  smoord  8353  fisupg  9249  winalim2  10682  relin01  11739  cshwlen  14838  aalioulem5  26478  musum  27333  chrelat2i  32695  bnj1173  35368  waj-ax  36903  sbn1ALT  37471  hlrelat2  40155  pm11.71  45087  onfrALTlem2  45235  19.41rg  45239  not12an2impnot1  45257  onfrALTlem2VD  45577  2pm13.193VD  45591  ax6e2eqVD  45595  ssfz12  48028