Theorem pm3.21 475

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  iba  531  ancr  550  anc2r  558  19.29r  1882  19.40b  1896  19.41v  1958  19.41  2233  2ax6elem  2469  mo3  2563  2mo  2649  relopabi  5692  smoord  8102  fisupg  8919  winalim2  10310  relin01  11356  cshwlen  14364  aalioulem5  25229  musum  26073  chrelat2i  30446  bnj1173  32695  waj-ax  34340  sbn1ALT  34779  hlrelat2  37154  pm11.71  41688  onfrALTlem2  41839  19.41rg  41843  not12an2impnot1  41861  onfrALTlem2VD  42182  2pm13.193VD  42196  ax6e2eqVD  42200  ssfz12  44479