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  2474  mo3  2564  2mo  2648  relopabi  5778  smoord  8305  fisupg  9198  winalim2  10619  relin01  11674  cshwlen  14761  aalioulem5  26302  musum  27154  chrelat2i  32436  bnj1173  35144  waj-ax  36596  sbn1ALT  37165  hlrelat2  39849  pm11.71  44824  onfrALTlem2  44973  19.41rg  44977  not12an2impnot1  44995  onfrALTlem2VD  45315  2pm13.193VD  45329  ax6e2eqVD  45333  ssfz12  47762