Theorem pm3.2 475

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm3.2i  476  pm3.43i  478  jca  521  jcad  522  ancl  554  hban  1906  19.29  1908  19.40b  1923  sban  2119  sb1  2510  mo4  2594  axia3  2722  r19.26  3126  difrab  4266  reuss2  4274  dmcosseq  5967  dmcosseqOLD  5968  soxp  8168  suppofssd  8248  smoord  8401  xpwdomg  9606  alephexp2  10693  lediv2a  12238  ssfzo12  13921  fzoopth  13924  r19.29uz  15547  isdrng5  21038  gsummoncoe1  22656  fbun  24189  fisshasheq  36060  isdrngo3  39085  cantnf2  44519  or3or  45215  pm11.71  45573  tratrb  45710  onfrALTlem3  45718  elex22VD  46012  en3lplem1VD  46016  tratrbVD  46034  undif3VD  46055  onfrALTlem3VD  46060  19.41rgVD  46075  2pm13.193VD  46076  ax6e2eqVD  46080  2uasbanhVD  46084  vk15.4jVD  46087