Theorem pm3.2 470

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm3.2i  471  pm3.43i  473  jca  516  jcad  517  ancl  549  19.29  1880  19.40b  1895  sban  2091  sb1  2486  mo4  2570  axia3  2699  r19.26  3100  difrab  4253  reuss2  4261  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  soxp  8076  suppofssd  8150  smoord  8302  xpwdomg  9497  alephexp2  10502  lediv2a  12048  ssfzo12  13712  fzoopth  13715  r19.29uz  15311  gsummoncoe1  22301  fbun  23830  fisshasheq  35350  isdrngo3  38333  cantnf2  43777  or3or  44474  pm11.71  44848  tratrb  44987  onfrALTlem3  44995  elex22VD  45289  en3lplem1VD  45293  tratrbVD  45311  undif3VD  45332  onfrALTlem3VD  45337  19.41rgVD  45352  2pm13.193VD  45353  ax6e2eqVD  45357  2uasbanhVD  45361  vk15.4jVD  45364