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

Theorem pm3.2i 257
Description: Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
pm3.2i.1 φ
pm3.2i.2 ψ
Assertion
Ref Expression
pm3.2i (φ ψ)

Proof of Theorem pm3.2i
StepHypRef Expression
1 pm3.2i.1 . 2 φ
2 pm3.2i.2 . 2 ψ
3 pm3.2 126 . 2 (φ → (ψ → (φ ψ)))
41, 2, 3mp2 16 1 (φ ψ)
Colors of variables: wff set class
Syntax hints:   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:  mp4an  405  pm4.87  481  biijust  557  3pm3.2i  1067  sbequilem  1701  unssi  3095  ssini  3137  bm1.3ii  3852  epelg  4001  onsucelsucexmid  4199  elvv  4329  funpr  4877  mpt2v  5517  caovcom  5581  th3q  6122  addnnnq0  6304  mulnnnq0  6305  nqprlu  6401  addsrpr  6492  mulsrpr  6493  bdbm1.3ii  7117
  Copyright terms: Public domain W3C validator