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  1874  19.40b  1888  19.41v  1949  19.41  2236  2ax6elem  2469  mo3  2558  2mo  2642  relopabi  5788  smoord  8337  fisupg  9242  winalim2  10656  relin01  11709  cshwlen  14771  aalioulem5  26251  musum  27108  chrelat2i  32301  bnj1173  34999  waj-ax  36409  sbn1ALT  36853  hlrelat2  39404  pm11.71  44393  onfrALTlem2  44543  19.41rg  44547  not12an2impnot1  44565  onfrALTlem2VD  44885  2pm13.193VD  44899  ax6e2eqVD  44903  ssfz12  47319