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  1909  19.40b  1923  19.41v  1984  19.41  2275  2ax6elem  2502  mo3  2592  2mo  2676  relopabiOLD  5806  smoord  8401  fisupg  9307  winalim2  10808  relin01  11867  cshwlen  14978  aalioulem5  26693  musum  27548  chrelat2i  32997  bnj1173  35702  waj-ax  37380  sbn1ALT  37948  hlrelat2  40652  pm11.71  45573  onfrALTlem2  45720  19.41rg  45724  not12an2impnot1  45742  onfrALTlem2VD  46062  2pm13.193VD  46076  ax6e2eqVD  46080  ssfz12  48589