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  2240  2ax6elem  2472  mo3  2561  2mo  2645  relopabi  5766  smoord  8291  fisupg  9179  winalim2  10594  relin01  11648  cshwlen  14708  aalioulem5  26272  musum  27129  chrelat2i  32347  bnj1173  35035  waj-ax  36479  sbn1ALT  36923  hlrelat2  39522  pm11.71  44514  onfrALTlem2  44663  19.41rg  44667  not12an2impnot1  44685  onfrALTlem2VD  45005  2pm13.193VD  45019  ax6e2eqVD  45023  ssfz12  47438