Theorem pm3.2 471

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  pm3.2i  472  pm3.43i  474  jca  513  jcad  514  ancl  546  19.29  1877  19.40b  1892  sban  2084  sb1  2478  mo4  2561  axia3  2691  r19.26  3112  r19.29OLD  3116  difrab  4309  reuss2  4316  dmcosseq  5973  fvn0fvelrnOLD  7161  soxp  8115  suppofssd  8188  smoord  8365  xpwdomg  9580  alephexp2  10576  lediv2a  12108  ssfzo12  13725  r19.29uz  15297  gsummoncoe1  21828  fbun  23344  fisshasheq  34104  isdrngo3  36827  cantnf2  42075  or3or  42774  pm11.71  43156  tratrb  43297  onfrALTlem3  43305  elex22VD  43600  en3lplem1VD  43604  tratrbVD  43622  undif3VD  43643  onfrALTlem3VD  43648  19.41rgVD  43663  2pm13.193VD  43664  ax6e2eqVD  43668  2uasbanhVD  43672  vk15.4jVD  43675  fzoopth  46035