Theorem pm3.2 473

Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. Its associated inference is pm3.2i 474 and its associated deduction is jca 519 (and the double deduction is jcad 520). 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 416	1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  pm3.2i  474  pm3.43i  476  jca  519  jcad  520  ancl  552  19.29  1892  19.40b  1907  sban  2112  sb1  2508  mo4  2592  axia3  2720  r19.26  3121  difrab  4270  reuss2  4278  dmcosseq  5952  dmcosseqOLD  5953  dmcosseqOLDOLD  5954  soxp  8104  suppofssd  8178  smoord  8331  xpwdomg  9530  alephexp2  10536  lediv2a  12083  ssfzo12  13762  fzoopth  13765  r19.29uz  15361  gsummoncoe1  22351  fbun  23880  fisshasheq  35429  isdrngo3  38422  cantnf2  43866  or3or  44563  pm11.71  44937  tratrb  45076  onfrALTlem3  45084  elex22VD  45378  en3lplem1VD  45382  tratrbVD  45400  undif3VD  45421  onfrALTlem3VD  45426  19.41rgVD  45441  2pm13.193VD  45442  ax6e2eqVD  45446  2uasbanhVD  45450  vk15.4jVD  45453