Theorem pm3.21 472

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  iba  532  ancr  551  anc2r  559  19.29r  1881  19.40b  1895  19.41v  1956  19.41  2247  2ax6elem  2478  mo3  2568  2mo  2652  relopabi  5772  smoord  8302  fisupg  9195  winalim2  10617  relin01  11672  cshwlen  14759  aalioulem5  26327  musum  27179  chrelat2i  32461  bnj1173  35191  waj-ax  36649  sbn1ALT  37218  hlrelat2  39902  pm11.71  44848  onfrALTlem2  44997  19.41rg  45001  not12an2impnot1  45019  onfrALTlem2VD  45339  2pm13.193VD  45353  ax6e2eqVD  45357  ssfz12  47784