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

This theorem is referenced by:  pm3.2i  470  pm3.43i  472  jca  511  jcad  512  ancl  544  19.29  1874  19.40b  1889  sban  2085  sb1  2480  mo4  2563  axia3  2692  r19.26  3093  difrab  4267  reuss2  4275  dmcosseq  5921  dmcosseqOLD  5922  dmcosseqOLDOLD  5923  soxp  8065  suppofssd  8139  smoord  8291  xpwdomg  9478  alephexp2  10479  lediv2a  12023  ssfzo12  13661  fzoopth  13664  r19.29uz  15260  gsummoncoe1  22224  fbun  23756  fisshasheq  35180  isdrngo3  38019  cantnf2  43442  or3or  44140  pm11.71  44514  tratrb  44653  onfrALTlem3  44661  elex22VD  44955  en3lplem1VD  44959  tratrbVD  44977  undif3VD  44998  onfrALTlem3VD  45003  19.41rgVD  45018  2pm13.193VD  45019  ax6e2eqVD  45023  2uasbanhVD  45027  vk15.4jVD  45030