Theorem pm3.21 473

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  iba  529  ancr  548  anc2r  556  19.29r  1878  19.40b  1892  19.41v  1954  19.41  2229  2ax6elem  2470  mo3  2559  2mo  2645  relopabi  5823  smoord  8365  fisupg  9291  winalim2  10691  relin01  11738  cshwlen  14749  aalioulem5  25849  musum  26695  chrelat2i  31649  bnj1173  34044  waj-ax  35347  sbn1ALT  35785  hlrelat2  38322  pm11.71  43204  onfrALTlem2  43355  19.41rg  43359  not12an2impnot1  43377  onfrALTlem2VD  43698  2pm13.193VD  43712  ax6e2eqVD  43716  ssfz12  46070