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

Theorem pm3.2 472
 Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. Its associated inference is pm3.2i 473 and its associated deduction is jca 514 (and the double deduction is jcad 515). See pm3.2im 162 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 415 1 (𝜑 → (𝜓 → (𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  pm3.2i  473  pm3.43i  475  jca  514  jcad  515  ancl  547  19.29  1870  19.40b  1885  sban  2082  sb1  2499  mo4  2646  axia3  2778  r19.26  3170  r19.29  3254  difrab  4276  reuss2  4282  dmcosseq  5843  fvn0fvelrn  6924  soxp  7822  suppofssd  7866  smoord  8001  xpwdomg  9048  alephexp2  10002  lediv2a  11533  ssfzo12  13129  r19.29uz  14709  gsummoncoe1  20471  fbun  22447  fisshasheq  32352  isdrngo3  35236  or3or  40369  pm11.71  40727  tratrb  40868  onfrALTlem3  40876  elex22VD  41171  en3lplem1VD  41175  tratrbVD  41193  undif3VD  41214  onfrALTlem3VD  41219  19.41rgVD  41234  2pm13.193VD  41235  ax6e2eqVD  41239  2uasbanhVD  41243  vk15.4jVD  41246  fzoopth  43526
 Copyright terms: Public domain W3C validator