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 471
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 413 1 (𝜑 → (𝜓 → (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  iba  527  ancr  546  anc2r  554  19.29r  1874  19.40b  1888  19.41v  1949  19.41  2235  2ax6elem  2475  mo3  2564  2mo  2648  relopabi  5832  smoord  8405  fisupg  9324  winalim2  10736  relin01  11787  cshwlen  14837  aalioulem5  26378  musum  27234  chrelat2i  32384  bnj1173  35016  waj-ax  36415  sbn1ALT  36859  hlrelat2  39405  pm11.71  44416  onfrALTlem2  44566  19.41rg  44570  not12an2impnot1  44588  onfrALTlem2VD  44909  2pm13.193VD  44923  ax6e2eqVD  44927  ssfz12  47326
  Copyright terms: Public domain W3C validator