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  2080  sb1  2483  mo4  2566  axia3  2695  r19.26  3111  r19.29OLD  3115  difrab  4318  reuss2  4326  dmcosseq  5987  dmcosseqOLD  5988  fvn0fvelrnOLD  7183  soxp  8154  suppofssd  8228  smoord  8405  xpwdomg  9625  alephexp2  10621  lediv2a  12162  ssfzo12  13798  fzoopth  13801  r19.29uz  15389  gsummoncoe1  22312  fbun  23848  fisshasheq  35120  isdrngo3  37966  cantnf2  43338  or3or  44036  pm11.71  44416  tratrb  44556  onfrALTlem3  44564  elex22VD  44859  en3lplem1VD  44863  tratrbVD  44881  undif3VD  44902  onfrALTlem3VD  44907  19.41rgVD  44922  2pm13.193VD  44923  ax6e2eqVD  44927  2uasbanhVD  44931  vk15.4jVD  44934