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  1874  19.40b  1889  sban  2083  sb1  2478  mo4  2561  axia3  2690  r19.26  3092  difrab  4268  reuss2  4276  dmcosseq  5917  dmcosseqOLD  5918  dmcosseqOLDOLD  5919  soxp  8059  suppofssd  8133  smoord  8285  xpwdomg  9471  alephexp2  10469  lediv2a  12013  ssfzo12  13656  fzoopth  13659  r19.29uz  15255  gsummoncoe1  22221  fbun  23753  fisshasheq  35147  isdrngo3  37998  cantnf2  43357  or3or  44055  pm11.71  44429  tratrb  44568  onfrALTlem3  44576  elex22VD  44870  en3lplem1VD  44874  tratrbVD  44892  undif3VD  44913  onfrALTlem3VD  44918  19.41rgVD  44933  2pm13.193VD  44934  ax6e2eqVD  44938  2uasbanhVD  44942  vk15.4jVD  44945