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

Theorem pm3.21 448
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 447 . 2
21com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  pm3.22  449  iba  503  ancr  549  anc2r  556  pm5.31  588  19.41v  1771  19.41  1971  2ax6elem  2193  mo3  2323  2mo  2373  2moOLD  2374  smoord  7055  fisupg  7788  winalim2  9095  relin01  10102  cshwlen  12770  aalioulem5  22732  musum  23467  chrelat2i  27284  waj-ax  29879  pm11.71  31303  ssfz12  32330  onfrALTlem2  33318  19.41rg  33323  not12an2impnot1  33345  onfrALTlem2VD  33689  2pm13.193VD  33703  ax6e2eqVD  33707  bnj1173  34058  hlrelat2  35127
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 185  df-an 371
  Copyright terms: Public domain W3C validator