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  2508  mo4  2592  axia3  2720  r19.26  3123  difrab  4264  reuss2  4272  dmcosseq  5960  dmcosseqOLD  5961  soxp  8130  suppofssd  8204  smoord  8357  xpwdomg  9563  alephexp2  10647  lediv2a  12192  ssfzo12  13874  fzoopth  13877  r19.29uz  15498  isdrng5  20988  gsummoncoe1  22606  fbun  24139  fisshasheq  35872  isdrngo3  38861  cantnf2  44285  or3or  44982  pm11.71  45340  tratrb  45478  onfrALTlem3  45486  elex22VD  45780  en3lplem1VD  45784  tratrbVD  45802  undif3VD  45823  onfrALTlem3VD  45828  19.41rgVD  45843  2pm13.193VD  45844  ax6e2eqVD  45848  2uasbanhVD  45852  vk15.4jVD  45855