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 470
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 id 22 . 2 ((𝜓𝜑) → (𝜓𝜑))
21expcom 412 1 (𝜑 → (𝜓 → (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 206  df-an 395
This theorem is referenced by:  iba  526  ancr  545  anc2r  553  19.29r  1875  19.40b  1889  19.41v  1951  19.41  2226  2ax6elem  2467  mo3  2556  2mo  2642  relopabi  5823  smoord  8369  fisupg  9295  winalim2  10695  relin01  11744  cshwlen  14755  aalioulem5  26083  musum  26929  chrelat2i  31883  bnj1173  34309  waj-ax  35604  sbn1ALT  36042  hlrelat2  38579  pm11.71  43460  onfrALTlem2  43611  19.41rg  43615  not12an2impnot1  43633  onfrALTlem2VD  43954  2pm13.193VD  43968  ax6e2eqVD  43972  ssfz12  46322
  Copyright terms: Public domain W3C validator