Theorem pm3.2 137

Description: Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) (Proof shortened by Jia Ming, 17-Nov-2020.)

Assertion

Ref	Expression
pm3.2	⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))

Proof of Theorem pm3.2

Step	Hyp	Ref	Expression
1		ax-ia3 106	1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-ia3 106

This theorem is referenced by:  pm3.21  260  pm3.2i  266  pm3.43i  267  ibar  295  jca  300  jcad  301  ancl  311  imnan  657  pm3.2an3  1118  19.29  1552  r19.26  2490  r19.29  2499  difrab  3254  dmcosseq  4651  lediv2a  8092  ssfzo12  9362  r19.29uz  10079