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  2509  mo4  2593  axia3  2721  r19.26  3124  difrab  4267  reuss2  4275  dmcosseq  5966  dmcosseqOLD  5967  soxp  8131  suppofssd  8205  smoord  8358  xpwdomg  9561  alephexp2  10594  lediv2a  12137  ssfzo12  13819  fzoopth  13822  r19.29uz  15442  isdrng5  20923  gsummoncoe1  22539  fbun  24072  fisshasheq  35725  isdrngo3  38717  cantnf2  44174  or3or  44871  pm11.71  45229  tratrb  45367  onfrALTlem3  45375  elex22VD  45669  en3lplem1VD  45673  tratrbVD  45691  undif3VD  45712  onfrALTlem3VD  45717  19.41rgVD  45732  2pm13.193VD  45733  ax6e2eqVD  45737  2uasbanhVD  45741  vk15.4jVD  45744