Theorem pm3.2 471

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  pm3.2i  472  pm3.43i  474  jca  513  jcad  514  ancl  546  19.29  1877  19.40b  1892  sban  2084  sb1  2478  mo4  2561  axia3  2691  r19.26  3112  r19.29OLD  3116  difrab  4308  reuss2  4315  dmcosseq  5971  fvn0fvelrnOLD  7158  soxp  8112  suppofssd  8185  smoord  8362  xpwdomg  9577  alephexp2  10573  lediv2a  12105  ssfzo12  13722  r19.29uz  15294  gsummoncoe1  21820  fbun  23336  fisshasheq  34093  isdrngo3  36816  cantnf2  42061  or3or  42760  pm11.71  43142  tratrb  43283  onfrALTlem3  43291  elex22VD  43586  en3lplem1VD  43590  tratrbVD  43608  undif3VD  43629  onfrALTlem3VD  43634  19.41rgVD  43649  2pm13.193VD  43650  ax6e2eqVD  43654  2uasbanhVD  43658  vk15.4jVD  43661  fzoopth  46022