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	|- ( ph -> ( ps -> ( ph /\ ps ) ) )

Proof of Theorem pm3.2

Step	Hyp	Ref	Expression
1		ax-ia3 107	1 |- ( ph -> ( ps -> ( ph /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-ia3 107

This theorem is referenced by:  pm3.21  261  pm3.2i  267  pm3.43i  268  ibar  296  jca  301  jcad  302  ancl  312  imnan  662  pm3.2an3  1125  19.29  1563  r19.26  2511  r19.29  2520  difrab  3289  dmcosseq  4736  lediv2a  8453  ssfzo12  9784  r19.29uz  10540