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  1903  19.40b  1918  sban  2114  sb1  2510  mo4  2594  axia3  2722  r19.26  3125  difrab  4272  reuss2  4280  dmcosseq  5970  dmcosseqOLD  5971  soxp  8126  suppofssd  8200  smoord  8353  xpwdomg  9548  alephexp2  10567  lediv2a  12110  ssfzo12  13790  fzoopth  13793  r19.29uz  15404  gsummoncoe1  22449  fbun  23978  fisshasheq  35584  isdrngo3  38588  cantnf2  44032  or3or  44729  pm11.71  45087  tratrb  45225  onfrALTlem3  45233  elex22VD  45527  en3lplem1VD  45531  tratrbVD  45549  undif3VD  45570  onfrALTlem3VD  45575  19.41rgVD  45590  2pm13.193VD  45591  ax6e2eqVD  45595  2uasbanhVD  45599  vk15.4jVD  45602