Theorem pm3.2 462

Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. See pm3.2im 156 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 449	1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  pm3.21  463  pm3.2i  470  pm3.43i  471  ibar  524  jca  553  jcad  554  ancl  567  pm3.2an3OLD  1234  19.29  1789  19.40b  1804  19.42-1  2091  axia3  2577  r19.26  3046  r19.29  3054  difrab  3860  reuss2  3866  dmcosseq  5308  fvn0fvelrn  6335  soxp  7177  smoord  7349  xpwdomg  8373  alephexp2  9282  lediv2a  10796  ssfzo12  12427  r19.29uz  13938  gsummoncoe1  19495  fbun  21454  wlkdvspthlem  26137  usgra2adedgspthlem2  26140  usgrcyclnl2  26169  erclwwlkeqlen  26340  eupatrl  26495  isdrngo3  32928  pm5.31r  33159  or3or  37339  pm11.71  37619  tratrb  37767  onfrALTlem3  37780  elex22VD  38096  en3lplem1VD  38100  tratrbVD  38119  undif3VD  38140  onfrALTlem3VD  38145  19.41rgVD  38160  2pm13.193VD  38161  ax6e2eqVD  38165  2uasbanhVD  38169  vk15.4jVD  38172  fzoopth  40360