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  1874  19.40b  1889  sban  2085  sb1  2482  mo4  2566  axia3  2695  r19.26  3096  difrab  4270  reuss2  4278  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  soxp  8071  suppofssd  8145  smoord  8297  xpwdomg  9490  alephexp2  10492  lediv2a  12036  ssfzo12  13675  fzoopth  13678  r19.29uz  15274  gsummoncoe1  22252  fbun  23784  fisshasheq  35309  isdrngo3  38156  cantnf2  43563  or3or  44260  pm11.71  44634  tratrb  44773  onfrALTlem3  44781  elex22VD  45075  en3lplem1VD  45079  tratrbVD  45097  undif3VD  45118  onfrALTlem3VD  45123  19.41rgVD  45138  2pm13.193VD  45139  ax6e2eqVD  45143  2uasbanhVD  45147  vk15.4jVD  45150