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

Theorem pm3.21 475
 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 417 1 (𝜑 → (𝜓 → (𝜓𝜑)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 400 This theorem is referenced by:  iba  531  ancr  550  anc2r  558  19.29r  1875  19.40b  1889  19.41v  1950  19.41  2235  2ax6elem  2482  mo3  2623  2mo  2710  relopabi  5662  smoord  8003  fisupg  8768  winalim2  10125  relin01  11171  cshwlen  14172  aalioulem5  24976  musum  25820  chrelat2i  30192  bnj1173  32450  waj-ax  34022  hlrelat2  36850  pm11.71  41272  onfrALTlem2  41423  19.41rg  41427  not12an2impnot1  41445  onfrALTlem2VD  41766  2pm13.193VD  41780  ax6e2eqVD  41784  ssfz12  44039
 Copyright terms: Public domain W3C validator