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

This theorem is referenced by:  pm3.2i  470  pm3.43i  472  jca  511  jcad  512  ancl  544  19.29  1877  19.40b  1892  sban  2084  sb1  2479  mo4  2566  axia3  2696  r19.26  3094  r19.29  3183  difrab  4239  reuss2  4246  dmcosseq  5871  fvn0fvelrn  7017  soxp  7941  suppofssd  7990  smoord  8167  xpwdomg  9274  alephexp2  10268  lediv2a  11799  ssfzo12  13408  r19.29uz  14990  gsummoncoe1  21385  fbun  22899  fisshasheq  32973  isdrngo3  36044  or3or  41520  pm11.71  41904  tratrb  42045  onfrALTlem3  42053  elex22VD  42348  en3lplem1VD  42352  tratrbVD  42370  undif3VD  42391  onfrALTlem3VD  42396  19.41rgVD  42411  2pm13.193VD  42412  ax6e2eqVD  42416  2uasbanhVD  42420  vk15.4jVD  42423  fzoopth  44707