Theorem pm3.21 464

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		pm3.2 463	. 2 ⊢ (𝜓 → (𝜑 → (𝜓 ∧ 𝜑)))
2	1	com12 32	1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  pm3.22  465  iba  524  ancr  572  anc2r  579  pm5.31  612  exan  1788  exanOLD  1789  19.29r  1802  19.40b  1815  19.41v  1914  19.41  2103  2ax6elem  2449  mo3  2507  2mo  2551  relopabi  5245  smoord  7462  fisupg  8208  fiinfg  8405  winalim2  9518  relin01  10552  cshwlen  13545  aalioulem5  24091  musum  24917  chrelat2i  29224  bnj1173  31070  waj-ax  32413  hlrelat2  34689  pm11.71  38597  onfrALTlem2  38761  19.41rg  38766  not12an2impnot1  38784  onfrALTlem2VD  39125  2pm13.193VD  39139  ax6e2eqVD  39143  ssfz12  41324