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  2468  mo3  2557  2mo  2641  relopabi  5785  smoord  8334  fisupg  9235  winalim2  10649  relin01  11702  cshwlen  14764  aalioulem5  26244  musum  27101  chrelat2i  32294  bnj1173  34992  waj-ax  36402  sbn1ALT  36846  hlrelat2  39397  pm11.71  44386  onfrALTlem2  44536  19.41rg  44540  not12an2impnot1  44558  onfrALTlem2VD  44878  2pm13.193VD  44892  ax6e2eqVD  44896  ssfz12  47315