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  656  pm3.2an3  1117  19.29  1551  r19.26  2485  r19.29  2494  difrab  3238  dmcosseq  4621  lediv2a  7973  ssfzo12  9233  r19.29uz  9878