Theorem pm3.2 130

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

Syntax hints:   → wi 4   ∧ wa 101

This theorem was proved from axioms:  ax-ia3 105

This theorem is referenced by:  pm3.21  255  pm3.2i  261  pm3.43i  262  ibar  289  jca  294  jcad  295  ancl  305  imnan  634  pm3.2an3  1094  19.29  1527  r19.26  2458  r19.29  2467  difrab  3238  dmcosseq  4630  lediv2a  7935  ssfzo12  9181  r19.29uz  9811