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

Theorem pm3.2 463
Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. See pm3.2im 157 for a version using only implication and negation. (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 450 1 (𝜑 → (𝜓 → (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  pm3.21  464  pm3.2i  471  pm3.43i  472  ibar  525  jca  554  jcad  555  ancl  568  pm3.2an3OLD  1239  19.29  1798  19.40b  1812  19.42-1  2102  axia3  2588  r19.26  3059  r19.29  3067  difrab  3883  reuss2  3889  dmcosseq  5357  fvn0fvelrn  6395  soxp  7250  smoord  7422  xpwdomg  8450  alephexp2  9363  lediv2a  10877  ssfzo12  12518  r19.29uz  14040  gsummoncoe1  19614  fbun  21584  isdrngo3  33429  pm5.31r  33660  or3or  37840  pm11.71  38118  tratrb  38267  onfrALTlem3  38280  elex22VD  38596  en3lplem1VD  38600  tratrbVD  38619  undif3VD  38640  onfrALTlem3VD  38645  19.41rgVD  38660  2pm13.193VD  38661  ax6e2eqVD  38665  2uasbanhVD  38669  vk15.4jVD  38672  fzoopth  40664
  Copyright terms: Public domain W3C validator