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

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
StepHypRef Expression
1 ax-ia3 106 1 (𝜑 → (𝜓 → (𝜑𝜓)))
Colors of variables: wff set class
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  657  pm3.2an3  1118  19.29  1552  r19.26  2490  r19.29  2499  difrab  3254  dmcosseq  4651  lediv2a  8092  ssfzo12  9362  r19.29uz  10079
  Copyright terms: Public domain W3C validator