Theorem pm3.2 470

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  pm3.2i  471  pm3.43i  473  jca  512  jcad  513  ancl  545  19.29  1876  19.40b  1891  sban  2083  sb1  2479  mo4  2566  axia3  2696  r19.26  3095  r19.29  3184  difrab  4242  reuss2  4249  dmcosseq  5882  fvn0fvelrn  7035  soxp  7970  suppofssd  8019  smoord  8196  xpwdomg  9344  alephexp2  10337  lediv2a  11869  ssfzo12  13480  r19.29uz  15062  gsummoncoe1  21475  fbun  22991  fisshasheq  33073  isdrngo3  36117  or3or  41631  pm11.71  42015  tratrb  42156  onfrALTlem3  42164  elex22VD  42459  en3lplem1VD  42463  tratrbVD  42481  undif3VD  42502  onfrALTlem3VD  42507  19.41rgVD  42522  2pm13.193VD  42523  ax6e2eqVD  42527  2uasbanhVD  42531  vk15.4jVD  42534  fzoopth  44819