Theorem pm3.2 126

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

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-ia3 101

This theorem is referenced by:  pm3.21  251  pm3.2i  257  pm3.43i  258  ibar  285  jca  290  jcad  291  ancl  301  imnan  624  pm3.2an3  1083  19.29  1511  r19.26  2441  r19.29  2450  difrab  3211  dmcosseq  4603  lediv2a  7861  ssfzo12  9080  r19.29uz  9590