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  2271  2ax6elem  2499  mo3  2589  2mo  2673  relopabi  5803  smoord  8355  fisupg  9259  winalim2  10706  relin01  11763  cshwlen  14871  aalioulem5  26573  musum  27428  chrelat2i  32847  bnj1173  35512  waj-ax  37034  sbn1ALT  37602  hlrelat2  40277  pm11.71  45222  onfrALTlem2  45370  19.41rg  45374  not12an2impnot1  45392  onfrALTlem2VD  45712  2pm13.193VD  45726  ax6e2eqVD  45730  ssfz12  48203