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

This theorem is referenced by:  iba  527  ancr  546  anc2r  554  19.29r  1875  19.40b  1889  19.41v  1950  19.41  2242  2ax6elem  2474  mo3  2564  2mo  2648  relopabi  5771  smoord  8297  fisupg  9188  winalim2  10607  relin01  11661  cshwlen  14722  aalioulem5  26300  musum  27157  chrelat2i  32440  bnj1173  35158  waj-ax  36608  sbn1ALT  37059  hlrelat2  39659  pm11.71  44634  onfrALTlem2  44783  19.41rg  44787  not12an2impnot1  44805  onfrALTlem2VD  45125  2pm13.193VD  45139  ax6e2eqVD  45143  ssfz12  47556