Theorem pm3.2 472

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm3.2i  473  pm3.43i  475  jca  514  jcad  515  ancl  547  19.29  1870  19.40b  1885  sban  2082  sb1  2499  mo4  2646  axia3  2778  r19.26  3170  r19.29  3254  difrab  4277  reuss2  4283  dmcosseq  5839  fvn0fvelrn  6920  soxp  7817  suppofssd  7861  smoord  7996  xpwdomg  9043  alephexp2  9997  lediv2a  11528  ssfzo12  13124  r19.29uz  14704  gsummoncoe1  20466  fbun  22442  fisshasheq  32347  isdrngo3  35231  or3or  40364  pm11.71  40722  tratrb  40863  onfrALTlem3  40871  elex22VD  41166  en3lplem1VD  41170  tratrbVD  41188  undif3VD  41209  onfrALTlem3VD  41214  19.41rgVD  41229  2pm13.193VD  41230  ax6e2eqVD  41234  2uasbanhVD  41238  vk15.4jVD  41241  fzoopth  43520