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 470
Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. Its associated inference is pm3.2i 471 and its associated deduction is jca 512 (and the double deduction is jcad 513). 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 413 1 (𝜑 → (𝜓 → (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  pm3.2i  471  pm3.43i  473  jca  512  jcad  513  ancl  545  19.29  1865  19.40b  1880  sban  2077  sb1  2496  mo4  2643  axia3  2775  r19.26  3167  r19.29  3251  difrab  4274  reuss2  4280  dmcosseq  5837  fvn0fvelrn  6917  soxp  7812  suppofssd  7856  smoord  7991  xpwdomg  9037  alephexp2  9991  lediv2a  11522  ssfzo12  13118  r19.29uz  14698  gsummoncoe1  20400  fbun  22376  fisshasheq  32249  isdrngo3  35118  or3or  40249  pm11.71  40606  tratrb  40747  onfrALTlem3  40755  elex22VD  41050  en3lplem1VD  41054  tratrbVD  41072  undif3VD  41093  onfrALTlem3VD  41098  19.41rgVD  41113  2pm13.193VD  41114  ax6e2eqVD  41118  2uasbanhVD  41122  vk15.4jVD  41125  fzoopth  43404
  Copyright terms: Public domain W3C validator