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 515 (and the double deduction is jcad 516). See pm3.2im 163 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 210  df-an 400

This theorem is referenced by:  pm3.2i  474  pm3.43i  476  jca  515  jcad  516  ancl  548  19.29  1874  19.40b  1889  sban  2085  sb1  2492  mo4  2625  axia3  2757  r19.26  3137  r19.29  3216  difrab  4229  reuss2  4235  dmcosseq  5809  fvn0fvelrn  6902  soxp  7806  suppofssd  7850  smoord  7985  xpwdomg  9033  alephexp2  9992  lediv2a  11523  ssfzo12  13125  r19.29uz  14702  gsummoncoe1  20933  fbun  22445  fisshasheq  32462  isdrngo3  35397  or3or  40724  pm11.71  41101  tratrb  41242  onfrALTlem3  41250  elex22VD  41545  en3lplem1VD  41549  tratrbVD  41567  undif3VD  41588  onfrALTlem3VD  41593  19.41rgVD  41608  2pm13.193VD  41609  ax6e2eqVD  41613  2uasbanhVD  41617  vk15.4jVD  41620  fzoopth  43884