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

This theorem is referenced by:  pm3.2i  470  pm3.43i  472  jca  511  jcad  512  ancl  544  19.29  1872  19.40b  1887  sban  2080  sb1  2486  mo4  2569  axia3  2698  r19.26  3117  r19.29OLD  3121  difrab  4337  reuss2  4345  dmcosseq  5999  dmcosseqOLD  6000  fvn0fvelrnOLD  7197  soxp  8170  suppofssd  8244  smoord  8421  xpwdomg  9654  alephexp2  10650  lediv2a  12189  ssfzo12  13809  fzoopth  13812  r19.29uz  15399  gsummoncoe1  22333  fbun  23869  fisshasheq  35082  isdrngo3  37919  cantnf2  43287  or3or  43985  pm11.71  44366  tratrb  44507  onfrALTlem3  44515  elex22VD  44810  en3lplem1VD  44814  tratrbVD  44832  undif3VD  44853  onfrALTlem3VD  44858  19.41rgVD  44873  2pm13.193VD  44874  ax6e2eqVD  44878  2uasbanhVD  44882  vk15.4jVD  44885