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  1876  19.40b  1890  19.41v  1951  19.41  2243  2ax6elem  2475  mo3  2565  2mo  2649  relopabi  5771  smoord  8298  fisupg  9191  winalim2  10610  relin01  11665  cshwlen  14752  aalioulem5  26313  musum  27168  chrelat2i  32451  bnj1173  35160  waj-ax  36612  sbn1ALT  37181  hlrelat2  39863  pm11.71  44842  onfrALTlem2  44991  19.41rg  44995  not12an2impnot1  45013  onfrALTlem2VD  45333  2pm13.193VD  45347  ax6e2eqVD  45351  ssfz12  47774