Theorem pm3.2 469

Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. Its associated inference is pm3.2i 470 and its associated deduction is jca 511 (and the double deduction is jcad 512). See pm3.2im 160 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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2	1	ex 412	1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm3.2i  470  pm3.43i  472  jca  511  jcad  512  ancl  544  19.29  1875  19.40b  1890  sban  2086  sb1  2483  mo4  2567  axia3  2696  r19.26  3098  difrab  4259  reuss2  4267  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  soxp  8072  suppofssd  8146  smoord  8298  xpwdomg  9493  alephexp2  10495  lediv2a  12041  ssfzo12  13705  fzoopth  13708  r19.29uz  15304  gsummoncoe1  22283  fbun  23815  fisshasheq  35313  isdrngo3  38294  cantnf2  43771  or3or  44468  pm11.71  44842  tratrb  44981  onfrALTlem3  44989  elex22VD  45283  en3lplem1VD  45287  tratrbVD  45305  undif3VD  45326  onfrALTlem3VD  45331  19.41rgVD  45346  2pm13.193VD  45347  ax6e2eqVD  45351  2uasbanhVD  45355  vk15.4jVD  45358