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

This theorem is referenced by:  pm3.2i  470  pm3.43i  472  jca  511  jcad  512  ancl  544  19.29  1868  19.40b  1883  sban  2075  sb1  2469  mo4  2552  axia3  2682  r19.26  3103  r19.29OLD  3107  difrab  4300  reuss2  4307  dmcosseq  5962  fvn0fvelrnOLD  7153  soxp  8109  suppofssd  8183  smoord  8360  xpwdomg  9576  alephexp2  10572  lediv2a  12105  ssfzo12  13722  r19.29uz  15294  gsummoncoe1  22149  fbun  23666  fisshasheq  34593  isdrngo3  37317  cantnf2  42564  or3or  43263  pm11.71  43645  tratrb  43786  onfrALTlem3  43794  elex22VD  44089  en3lplem1VD  44093  tratrbVD  44111  undif3VD  44132  onfrALTlem3VD  44137  19.41rgVD  44152  2pm13.193VD  44153  ax6e2eqVD  44157  2uasbanhVD  44161  vk15.4jVD  44164  fzoopth  46520