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  1876  19.40b  1890  19.41v  1951  19.41  2243  2ax6elem  2475  mo3  2565  2mo  2649  relopabi  5779  smoord  8307  fisupg  9200  winalim2  10619  relin01  11673  cshwlen  14734  aalioulem5  26312  musum  27169  chrelat2i  32452  bnj1173  35177  waj-ax  36627  sbn1ALT  37100  hlrelat2  39773  pm11.71  44747  onfrALTlem2  44896  19.41rg  44900  not12an2impnot1  44918  onfrALTlem2VD  45238  2pm13.193VD  45252  ax6e2eqVD  45256  ssfz12  47668