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  403  pm4.87  493  biijust  569  3pm3.2i  1081  sbequilem  1716  unssi  3112  ssini  3154  bm1.3ii  3869  epelg  4018  onsucelsucexmid  4215  elvv  4345  funpr  4894  mpt2v  5536  caovcom  5600  th3q  6147  endisj  6234  addnnnq0  6431  mulnnnq0  6432  nqprxx  6529  addsrpr  6633  mulsrpr  6634  apreim  7347  mulcanapi  7390  div1  7422  recdivap  7436  divdivap1  7441  divdivap2  7442  divassapi  7486  divdirapi  7487  div23api  7488  div11api  7489  divmuldivapi  7490  divmul13api  7491  divadddivapi  7492  divdivdivapi  7493  lemulge11  7573  2cnne0  7872  2rene0  7873  1mhlfehlf  7880  halfpm6th  7882  2halves  7891  halfaddsub  7896  avglt1  7900  avglt2  7901  nneoor  8076  zeo  8079  frecfzennn  8844  expge1  8906  cjreb  9054  bdbm1.3ii  9279
  Copyright terms: Public domain W3C validator