Theorem pm3.2 139

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 108	1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-ia3 108

This theorem is referenced by:  pm3.21  264  pm3.2i  272  pm3.43i  273  ibar  301  jca  306  jcad  307  ancl  318  imnan  692  pm3.2an3  1179  19.29  1644  r19.26  2633  r19.29  2644  difrab  3448  dmcosseq  4955  lediv2a  8975  ssfzo12  10360  r19.29uz  11347