Theorem pm3.2 463

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  pm3.2i  464  pm3.43i  466  jca  509  jcad  510  ibar  526  ancl  542  19.29  1978  19.40b  1992  19.42-1OLD  2281  axia3  2790  r19.26  3274  r19.29  3282  difrab  4130  reuss2  4136  dmcosseq  5620  fvn0fvelrn  6681  soxp  7554  smoord  7728  xpwdomg  8759  alephexp2  9718  lediv2a  11247  ssfzo12  12856  r19.29uz  14467  gsummoncoe1  20034  fbun  22014  isdrngo3  34300  pm5.31r  34933  or3or  39159  pm11.71  39437  tratrb  39580  onfrALTlem3  39588  elex22VD  39893  en3lplem1VD  39897  tratrbVD  39915  undif3VD  39936  onfrALTlem3VD  39941  19.41rgVD  39956  2pm13.193VD  39957  ax6e2eqVD  39961  2uasbanhVD  39965  vk15.4jVD  39968  fzoopth  42225