ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm3.2 Unicode version

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
StepHypRef Expression
1 ax-ia3 107 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator