Theorem pm3.2 475

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm3.2i  476  pm3.43i  478  jca  521  jcad  522  ancl  554  19.29  1906  19.40b  1921  sban  2117  sb1  2513  mo4  2597  axia3  2725  r19.26  3128  difrab  4274  reuss2  4282  dmcosseq  5973  dmcosseqOLD  5974  soxp  8134  suppofssd  8208  smoord  8361  xpwdomg  9557  alephexp2  10584  lediv2a  12127  ssfzo12  13807  fzoopth  13810  r19.29uz  15428  isdrng5  20891  gsummoncoe1  22505  fbun  24034  fisshasheq  35629  isdrngo3  38651  cantnf2  44093  or3or  44790  pm11.71  45148  tratrb  45286  onfrALTlem3  45294  elex22VD  45588  en3lplem1VD  45592  tratrbVD  45610  undif3VD  45631  onfrALTlem3VD  45636  19.41rgVD  45651  2pm13.193VD  45652  ax6e2eqVD  45656  2uasbanhVD  45660  vk15.4jVD  45663