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 457
Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. Its associated inference is pm3.2i 458 and its associated deduction is jca 503 (and the double deduction is jcad 504). See pm3.2im 158 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 399 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 198  df-an 385
This theorem is referenced by:  pm3.2i  458  pm3.43i  460  jca  503  jcad  504  ibar  520  ancl  536  19.29  1963  19.40b  1977  19.42-1  2273  axia3  2782  r19.26  3263  r19.29  3271  difrab  4113  reuss2  4119  dmcosseq  5602  fvn0fvelrn  6664  soxp  7534  smoord  7708  xpwdomg  8739  alephexp2  9698  lediv2a  11212  ssfzo12  12805  r19.29uz  14333  gsummoncoe1  19902  fbun  21878  isdrngo3  34088  pm5.31r  34656  or3or  38837  pm11.71  39115  tratrb  39262  onfrALTlem3  39275  elex22VD  39586  en3lplem1VD  39590  tratrbVD  39609  undif3VD  39630  onfrALTlem3VD  39635  19.41rgVD  39650  2pm13.193VD  39651  ax6e2eqVD  39655  2uasbanhVD  39659  vk15.4jVD  39662  fzoopth  41930
  Copyright terms: Public domain W3C validator