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  1937  exanOLD  1938  19.29r  1951  19.40b  1964  19.41v  2026  19.41vOLD  2079  19.41  2250  2ax6elem  2586  mo3  2645  2mo  2689  relopabi  5401  smoord  7632  fisupg  8375  fiinfg  8572  winalim2  9730  relin01  10764  cshwlen  13765  aalioulem5  24310  musum  25137  chrelat2i  29554  bnj1173  31398  waj-ax  32740  hlrelat2  35210  pm11.71  39117  onfrALTlem2  39281  19.41rg  39286  not12an2impnot1  39304  onfrALTlem2VD  39642  2pm13.193VD  39656  ax6e2eqVD  39660  ssfz12  41852
  Copyright terms: Public domain W3C validator