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 461
Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. See pm3.2im 155 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 448 1 (𝜑 → (𝜓 → (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  pm3.21  462  pm3.2i  469  pm3.43i  470  ibar  523  jca  552  jcad  553  ancl  566  pm3.2an3OLD  1233  19.29  1788  19.40b  1803  19.42-1  2089  axia3  2573  r19.26  3042  r19.29  3050  difrab  3856  reuss2  3862  dmcosseq  5292  fvn0fvelrn  6310  soxp  7151  smoord  7323  xpwdomg  8347  alephexp2  9256  lediv2a  10763  ssfzo12  12379  r19.29uz  13881  gsummoncoe1  19438  fbun  21393  wlkdvspthlem  25900  usgra2adedgspthlem2  25903  usgrcyclnl2  25932  erclwwlkeqlen  26103  eupatrl  26258  isdrngo3  32728  pm5.31r  32959  or3or  37139  pm11.71  37419  tratrb  37567  onfrALTlem3  37580  elex22VD  37896  en3lplem1VD  37900  tratrbVD  37919  undif3VD  37940  onfrALTlem3VD  37945  19.41rgVD  37960  2pm13.193VD  37961  ax6e2eqVD  37965  2uasbanhVD  37969  vk15.4jVD  37972  fzoopth  40184
  Copyright terms: Public domain W3C validator