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  1873  19.40b  1887  19.41v  1949  19.41  2236  2ax6elem  2478  mo3  2567  2mo  2651  relopabi  5846  smoord  8421  fisupg  9352  winalim2  10765  relin01  11814  cshwlen  14847  aalioulem5  26396  musum  27252  chrelat2i  32397  bnj1173  34978  waj-ax  36380  sbn1ALT  36824  hlrelat2  39360  pm11.71  44366  onfrALTlem2  44517  19.41rg  44521  not12an2impnot1  44539  onfrALTlem2VD  44860  2pm13.193VD  44874  ax6e2eqVD  44878  ssfz12  47229