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  2477  mo4  2560  axia3  2689  r19.26  3092  r19.29OLD  3096  difrab  4284  reuss2  4292  dmcosseq  5943  dmcosseqOLD  5944  fvn0fvelrnOLD  7138  soxp  8111  suppofssd  8185  smoord  8337  xpwdomg  9545  alephexp2  10541  lediv2a  12084  ssfzo12  13727  fzoopth  13730  r19.29uz  15324  gsummoncoe1  22202  fbun  23734  fisshasheq  35109  isdrngo3  37960  cantnf2  43321  or3or  44019  pm11.71  44393  tratrb  44533  onfrALTlem3  44541  elex22VD  44835  en3lplem1VD  44839  tratrbVD  44857  undif3VD  44878  onfrALTlem3VD  44883  19.41rgVD  44898  2pm13.193VD  44899  ax6e2eqVD  44903  2uasbanhVD  44907  vk15.4jVD  44910