MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm3.21 Structured version   Visualization version   GIF version

Theorem pm3.21 463
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
StepHypRef Expression
1 pm3.2 462 . 2 (𝜓 → (𝜑 → (𝜓𝜑)))
21com12 32 1 (𝜑 → (𝜓 → (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  pm3.22  464  iba  525  ancr  573  anc2r  580  pm5.31  613  exan  1901  exanOLD  1902  19.29r  1915  19.40b  1928  19.41v  1990  19.41vOLD  2043  19.41  2214  2ax6elem  2550  mo3  2609  2mo  2653  relopabi  5353  smoord  7582  fisupg  8324  fiinfg  8521  winalim2  9631  relin01  10665  cshwlen  13666  aalioulem5  24211  musum  25037  chrelat2i  29454  bnj1173  31298  waj-ax  32640  hlrelat2  35109  pm11.71  39016  onfrALTlem2  39180  19.41rg  39185  not12an2impnot1  39203  onfrALTlem2VD  39541  2pm13.193VD  39555  ax6e2eqVD  39559  ssfz12  41751
  Copyright terms: Public domain W3C validator