Theorem pm3.2 474

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  pm3.2i  475  pm3.43i  477  jca  520  jcad  521  ancl  553  19.29  1896  19.40b  1911  sban  2116  sb1  2512  mo4  2596  axia3  2724  r19.26  3125  difrab  4273  reuss2  4281  dmcosseq  5959  dmcosseqOLD  5960  soxp  8113  suppofssd  8187  smoord  8340  xpwdomg  9535  alephexp2  10554  lediv2a  12100  ssfzo12  13779  fzoopth  13782  r19.29uz  15392  gsummoncoe1  22429  fbun  23958  fisshasheq  35477  isdrngo3  38470  cantnf2  43914  or3or  44611  pm11.71  44971  tratrb  45110  onfrALTlem3  45118  elex22VD  45412  en3lplem1VD  45416  tratrbVD  45434  undif3VD  45455  onfrALTlem3VD  45460  19.41rgVD  45475  2pm13.193VD  45476  ax6e2eqVD  45480  2uasbanhVD  45484  vk15.4jVD  45487