Theorem pm3.2 469

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm3.2i  470  pm3.43i  472  jca  511  jcad  512  ancl  544  19.29  1875  19.40b  1890  sban  2086  sb1  2482  mo4  2566  axia3  2695  r19.26  3097  difrab  4258  reuss2  4266  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  soxp  8079  suppofssd  8153  smoord  8305  xpwdomg  9500  alephexp2  10504  lediv2a  12050  ssfzo12  13714  fzoopth  13717  r19.29uz  15313  gsummoncoe1  22273  fbun  23805  fisshasheq  35297  isdrngo3  38280  cantnf2  43753  or3or  44450  pm11.71  44824  tratrb  44963  onfrALTlem3  44971  elex22VD  45265  en3lplem1VD  45269  tratrbVD  45287  undif3VD  45308  onfrALTlem3VD  45313  19.41rgVD  45328  2pm13.193VD  45329  ax6e2eqVD  45333  2uasbanhVD  45337  vk15.4jVD  45340