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  1870  19.40b  1885  sban  2077  sb1  2480  mo4  2563  axia3  2692  r19.26  3108  r19.29OLD  3112  difrab  4323  reuss2  4331  dmcosseq  5989  dmcosseqOLD  5990  fvn0fvelrnOLD  7182  soxp  8152  suppofssd  8226  smoord  8403  xpwdomg  9622  alephexp2  10618  lediv2a  12159  ssfzo12  13794  fzoopth  13797  r19.29uz  15385  gsummoncoe1  22327  fbun  23863  fisshasheq  35098  isdrngo3  37945  cantnf2  43314  or3or  44012  pm11.71  44392  tratrb  44533  onfrALTlem3  44541  elex22VD  44836  en3lplem1VD  44840  tratrbVD  44858  undif3VD  44879  onfrALTlem3VD  44884  19.41rgVD  44899  2pm13.193VD  44900  ax6e2eqVD  44904  2uasbanhVD  44908  vk15.4jVD  44911