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  1873  19.40b  1888  sban  2081  sb1  2476  mo4  2559  axia3  2688  r19.26  3091  r19.29OLD  3095  difrab  4281  reuss2  4289  dmcosseq  5940  dmcosseqOLD  5941  fvn0fvelrnOLD  7135  soxp  8108  suppofssd  8182  smoord  8334  xpwdomg  9538  alephexp2  10534  lediv2a  12077  ssfzo12  13720  fzoopth  13723  r19.29uz  15317  gsummoncoe1  22195  fbun  23727  fisshasheq  35102  isdrngo3  37953  cantnf2  43314  or3or  44012  pm11.71  44386  tratrb  44526  onfrALTlem3  44534  elex22VD  44828  en3lplem1VD  44832  tratrbVD  44850  undif3VD  44871  onfrALTlem3VD  44876  19.41rgVD  44891  2pm13.193VD  44892  ax6e2eqVD  44896  2uasbanhVD  44900  vk15.4jVD  44903