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  19.29  1905  19.40b  1920  sban  2116  sb1  2507  mo4  2591  axia3  2719  r19.26  3122  difrab  4263  reuss2  4271  dmcosseq  5959  dmcosseqOLD  5960  soxp  8143  suppofssd  8223  smoord  8376  xpwdomg  9582  alephexp2  10669  lediv2a  12214  ssfzo12  13897  fzoopth  13900  r19.29uz  15523  isdrng5  21013  gsummoncoe1  22631  fbun  24164  fisshasheq  35979  isdrngo3  38986  cantnf2  44420  or3or  45116  pm11.71  45474  tratrb  45612  onfrALTlem3  45620  elex22VD  45914  en3lplem1VD  45918  tratrbVD  45936  undif3VD  45957  onfrALTlem3VD  45962  19.41rgVD  45977  2pm13.193VD  45978  ax6e2eqVD  45982  2uasbanhVD  45986  vk15.4jVD  45989