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  2235  2ax6elem  2474  mo3  2563  2mo  2647  relopabi  5801  smoord  8379  fisupg  9296  winalim2  10710  relin01  11761  cshwlen  14817  aalioulem5  26296  musum  27153  chrelat2i  32346  bnj1173  35033  waj-ax  36432  sbn1ALT  36876  hlrelat2  39422  pm11.71  44421  onfrALTlem2  44571  19.41rg  44575  not12an2impnot1  44593  onfrALTlem2VD  44913  2pm13.193VD  44927  ax6e2eqVD  44931  ssfz12  47343