Theorem pm3.2 138

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-ia3 107

This theorem is referenced by:  pm3.21  262  pm3.2i  270  pm3.43i  271  ibar  299  jca  304  jcad  305  ancl  316  imnan  679  pm3.2an3  1160  19.29  1599  r19.26  2556  r19.29  2567  difrab  3345  dmcosseq  4805  lediv2a  8646  ssfzo12  9994  r19.29uz  10757