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  1876  19.40b  1890  19.41v  1952  19.41  2227  2ax6elem  2468  mo3  2557  2mo  2643  relopabi  5822  smoord  8371  fisupg  9297  winalim2  10697  relin01  11745  cshwlen  14756  aalioulem5  26099  musum  26946  chrelat2i  31900  bnj1173  34326  waj-ax  35615  sbn1ALT  36053  hlrelat2  38590  pm11.71  43471  onfrALTlem2  43622  19.41rg  43626  not12an2impnot1  43644  onfrALTlem2VD  43965  2pm13.193VD  43979  ax6e2eqVD  43983  ssfz12  46333