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

Theorem pm3.2 130
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 105 1 (𝜑 → (𝜓 → (𝜑𝜓)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-ia3 105
This theorem is referenced by:  pm3.21  255  pm3.2i  261  pm3.43i  262  ibar  289  jca  294  jcad  295  ancl  305  imnan  634  pm3.2an3  1094  19.29  1527  r19.26  2458  r19.29  2467  difrab  3238  dmcosseq  4630  lediv2a  7935  ssfzo12  9181  r19.29uz  9811
  Copyright terms: Public domain W3C validator