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  2272  2ax6elem  2500  mo3  2590  2mo  2674  relopabi  5800  smoord  8357  fisupg  9263  winalim2  10762  relin01  11821  cshwlen  14930  aalioulem5  26645  musum  27500  chrelat2i  32949  bnj1173  35615  waj-ax  37172  sbn1ALT  37740  hlrelat2  40428  pm11.71  45340  onfrALTlem2  45488  19.41rg  45492  not12an2impnot1  45510  onfrALTlem2VD  45830  2pm13.193VD  45844  ax6e2eqVD  45848  ssfz12  48328