Theorem pm3.21 472

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 414	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  iba  528  ancr  547  anc2r  555  19.29r  1877  19.40b  1891  19.41v  1953  19.41  2228  2ax6elem  2468  mo3  2557  2mo  2643  relopabi  5783  smoord  8316  fisupg  9242  winalim2  10641  relin01  11688  cshwlen  14699  aalioulem5  25733  musum  26577  chrelat2i  31370  bnj1173  33703  waj-ax  34962  sbn1ALT  35400  hlrelat2  37939  pm11.71  42799  onfrALTlem2  42950  19.41rg  42954  not12an2impnot1  42972  onfrALTlem2VD  43293  2pm13.193VD  43307  ax6e2eqVD  43311  ssfz12  45666