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

Theorem pm3.2 447
Description: Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
Assertion
Ref Expression
pm3.2

Proof of Theorem pm3.2
StepHypRef Expression
1 id 22 . 2
21ex 434 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  pm3.21  448  pm3.2i  455  pm3.43i  456  ibar  504  jca  532  jcad  533  ancl  546  pm3.2an3  1175  19.29  1683  axia3  2422  r19.26  2984  r19.29  2992  difrab  3771  dmcosseq  5269  fvn0fvelrn  6088  soxp  6913  smoord  7055  xpwdomg  8032  alephexp2  8977  lediv2a  10464  ssfzo12  11905  r19.29uz  13183  gsummoncoe1  18346  fbun  20341  wlkdvspthlem  24609  usgra2adedgspthlem2  24612  usgrcyclnl2  24641  erclwwlkeqlen  24812  eupatrl  24968  isdrngo3  30362  pm5.31r  30594  pm11.71  31303  fzoopth  32340  tratrb  33307  onfrALTlem3  33316  elex22VD  33639  en3lplem1VD  33643  tratrbVD  33661  undif3VD  33682  onfrALTlem3VD  33687  19.41rgVD  33702  2pm13.193VD  33703  ax6e2eqVD  33707  2uasbanhVD  33711  vk15.4jVD  33714
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