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  1872  19.40b  1886  19.41v  1947  19.41  2233  2ax6elem  2473  mo3  2562  2mo  2646  relopabi  5835  smoord  8404  fisupg  9322  winalim2  10734  relin01  11785  cshwlen  14834  aalioulem5  26393  musum  27249  chrelat2i  32394  bnj1173  34995  waj-ax  36397  sbn1ALT  36841  hlrelat2  39386  pm11.71  44393  onfrALTlem2  44544  19.41rg  44548  not12an2impnot1  44566  onfrALTlem2VD  44887  2pm13.193VD  44901  ax6e2eqVD  44905  ssfz12  47264
  Copyright terms: Public domain W3C validator