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

Theorem pm3.2 126
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.)
Assertion
Ref Expression
pm3.2 (φ → (ψ → (φ ψ)))

Proof of Theorem pm3.2
StepHypRef Expression
1 id 19 . 2 ((φ ψ) → (φ ψ))
21ex 108 1 (φ → (ψ → (φ ψ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  pm3.21  251  pm3.2i  257  pm3.43i  258  ibar  285  jca  290  jcad  291  ancl  301  imnan  623  pm3.2an3  1082  19.29  1508  r19.26  2435  r19.29  2444  difrab  3205  dmcosseq  4546  lediv2a  7602  ssfzo12  8810
  Copyright terms: Public domain W3C validator