ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm3.2i 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  6432  mulnnnq0  6433  nqprxx  6529  addsrpr  6673  mulsrpr  6674  apreim  7387  mulcanapi  7430  div1  7462  recdivap  7476  divdivap1  7481  divdivap2  7482  divassapi  7526  divdirapi  7527  div23api  7528  div11api  7529  divmuldivapi  7530  divmul13api  7531  divadddivapi  7532  divdivdivapi  7533  lemulge11  7613  2cnne0  7912  2rene0  7913  1mhlfehlf  7920  halfpm6th  7922  2halves  7931  halfaddsub  7936  avglt1  7940  avglt2  7941  nneoor  8116  zeo  8119  frecfzennn  8884  expge1  8946  cjreb  9094  bdbm1.3ii  9346
  Copyright terms: Public domain W3C validator