Theorem pm3.21 476

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 23	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜑))
2	1	expcom 418	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  iba  536  ancr  555  anc2r  563  19.29r  1897  19.40b  1911  19.41v  1972  19.41  2273  2ax6elem  2504  mo3  2594  2mo  2678  relopabi  5800  smoord  8340  fisupg  9236  winalim2  10669  relin01  11726  cshwlen  14826  aalioulem5  26458  musum  27313  chrelat2i  32626  bnj1173  35307  waj-ax  36787  sbn1ALT  37355  hlrelat2  40039  pm11.71  44971  onfrALTlem2  45120  19.41rg  45124  not12an2impnot1  45142  onfrALTlem2VD  45462  2pm13.193VD  45476  ax6e2eqVD  45480  ssfz12  47906