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  2482  mo4  2565  axia3  2694  r19.26  3098  r19.29OLD  3102  difrab  4293  reuss2  4301  dmcosseq  5956  dmcosseqOLD  5957  fvn0fvelrnOLD  7153  soxp  8128  suppofssd  8202  smoord  8379  xpwdomg  9599  alephexp2  10595  lediv2a  12136  ssfzo12  13775  fzoopth  13778  r19.29uz  15369  gsummoncoe1  22246  fbun  23778  fisshasheq  35137  isdrngo3  37983  cantnf2  43349  or3or  44047  pm11.71  44421  tratrb  44561  onfrALTlem3  44569  elex22VD  44863  en3lplem1VD  44867  tratrbVD  44885  undif3VD  44906  onfrALTlem3VD  44911  19.41rgVD  44926  2pm13.193VD  44927  ax6e2eqVD  44931  2uasbanhVD  44935  vk15.4jVD  44938