Theorem pm3.21 477

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 23	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜑))
2	1	expcom 419	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  iba  537  ancr  556  anc2r  564  19.29r  1907  19.40b  1921  19.41v  1982  19.41  2274  2ax6elem  2505  mo3  2595  2mo  2679  relopabi  5814  smoord  8361  fisupg  9258  winalim2  10699  relin01  11756  cshwlen  14862  aalioulem5  26536  musum  27392  chrelat2i  32754  bnj1173  35422  waj-ax  36966  sbn1ALT  37534  hlrelat2  40218  pm11.71  45148  onfrALTlem2  45296  19.41rg  45300  not12an2impnot1  45318  onfrALTlem2VD  45638  2pm13.193VD  45652  ax6e2eqVD  45656  ssfz12  48092