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

Theorem pm3.2 462
 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 449 1 (𝜑 → (𝜓 → (𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 385 This theorem is referenced by:  pm3.21  463  pm3.2i  470  pm3.43i  471  ibar  524  jca  553  jcad  554  ancl  568  19.29  1841  19.40b  1855  19.42-1  2142  axia3  2618  r19.26  3093  r19.29  3101  difrab  3934  reuss2  3940  dmcosseq  5419  fvn0fvelrn  6470  soxp  7335  smoord  7507  xpwdomg  8531  alephexp2  9441  lediv2a  10955  ssfzo12  12601  r19.29uz  14134  gsummoncoe1  19722  fbun  21691  extwwlkfab  27342  isdrngo3  33888  pm5.31r  34462  or3or  38636  pm11.71  38914  tratrb  39063  onfrALTlem3  39076  elex22VD  39388  en3lplem1VD  39392  tratrbVD  39411  undif3VD  39432  onfrALTlem3VD  39437  19.41rgVD  39452  2pm13.193VD  39453  ax6e2eqVD  39457  2uasbanhVD  39461  vk15.4jVD  39464  fzoopth  41662
 Copyright terms: Public domain W3C validator