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  2470  mo3  2564  2mo  2650  relopabi  5732  smoord  8196  fisupg  9062  winalim2  10452  relin01  11499  cshwlen  14512  aalioulem5  25496  musum  26340  chrelat2i  30727  bnj1173  32982  waj-ax  34603  sbn1ALT  35042  hlrelat2  37417  pm11.71  42015  onfrALTlem2  42166  19.41rg  42170  not12an2impnot1  42188  onfrALTlem2VD  42509  2pm13.193VD  42523  ax6e2eqVD  42527  ssfz12  44806