ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm3.2 GIF 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 (𝜑 → (𝜓 → (𝜑𝜓)))

Proof of Theorem pm3.2
StepHypRef Expression
1 ax-ia3 107 1 (𝜑 → (𝜓 → (𝜑𝜓)))
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  262  pm3.2i  270  pm3.43i  271  ibar  299  jca  304  jcad  305  ancl  316  imnan  680  pm3.2an3  1161  19.29  1600  r19.26  2561  r19.29  2572  difrab  3355  dmcosseq  4818  lediv2a  8677  ssfzo12  10032  r19.29uz  10796
  Copyright terms: Public domain W3C validator