Theorem pm3.21 471

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  iba  527  ancr  546  anc2r  554  19.29r  1875  19.40b  1889  19.41v  1950  19.41  2238  2ax6elem  2470  mo3  2559  2mo  2643  relopabi  5762  smoord  8285  fisupg  9172  winalim2  10584  relin01  11638  cshwlen  14703  aalioulem5  26269  musum  27126  chrelat2i  32340  bnj1173  35009  waj-ax  36447  sbn1ALT  36891  hlrelat2  39441  pm11.71  44429  onfrALTlem2  44578  19.41rg  44582  not12an2impnot1  44600  onfrALTlem2VD  44920  2pm13.193VD  44934  ax6e2eqVD  44938  ssfz12  47344