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  3089  difrab  4271  reuss2  4279  dmcosseq  5923  dmcosseqOLD  5924  dmcosseqOLDOLD  5925  fvn0fvelrnOLD  7101  soxp  8069  suppofssd  8143  smoord  8295  xpwdomg  9496  alephexp2  10494  lediv2a  12037  ssfzo12  13680  fzoopth  13683  r19.29uz  15276  gsummoncoe1  22211  fbun  23743  fisshasheq  35087  isdrngo3  37938  cantnf2  43298  or3or  43996  pm11.71  44370  tratrb  44510  onfrALTlem3  44518  elex22VD  44812  en3lplem1VD  44816  tratrbVD  44834  undif3VD  44855  onfrALTlem3VD  44860  19.41rgVD  44875  2pm13.193VD  44876  ax6e2eqVD  44880  2uasbanhVD  44884  vk15.4jVD  44887