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 206  df-an 396

This theorem is referenced by:  iba  527  ancr  546  anc2r  554  19.29r  1878  19.40b  1892  19.41v  1954  19.41  2231  2ax6elem  2470  mo3  2564  2mo  2650  relopabi  5721  smoord  8167  fisupg  8992  winalim2  10383  relin01  11429  cshwlen  14440  aalioulem5  25401  musum  26245  chrelat2i  30628  bnj1173  32882  waj-ax  34530  sbn1ALT  34969  hlrelat2  37344  pm11.71  41904  onfrALTlem2  42055  19.41rg  42059  not12an2impnot1  42077  onfrALTlem2VD  42398  2pm13.193VD  42412  ax6e2eqVD  42416  ssfz12  44694