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  5769  smoord  8294  fisupg  9182  winalim2  10597  relin01  11651  cshwlen  14716  aalioulem5  26281  musum  27138  chrelat2i  32356  bnj1173  35025  waj-ax  36469  sbn1ALT  36913  hlrelat2  39512  pm11.71  44504  onfrALTlem2  44653  19.41rg  44657  not12an2impnot1  44675  onfrALTlem2VD  44995  2pm13.193VD  45009  ax6e2eqVD  45013  ssfz12  47428