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  570  3pm3.2i  1082  sbequilem  1719  unssi  3118  ssini  3160  bm1.3ii  3878  epelg  4027  onsucelsucexmid  4255  elvv  4402  funpr  4951  mpt2v  5594  caovcom  5658  th3q  6211  endisj  6298  phplem2  6316  addnnnq0  6545  mulnnnq0  6546  nqprxx  6642  addsrpr  6828  mulsrpr  6829  recidpirq  6932  apreim  7592  mulcanapi  7646  div1  7678  recdivap  7692  divdivap1  7697  divdivap2  7698  divassapi  7742  divdirapi  7743  div23api  7744  div11api  7745  divmuldivapi  7746  divmul13api  7747  divadddivapi  7748  divdivdivapi  7749  lemulge11  7830  2cnne0  8132  2rene0  8133  1mhlfehlf  8141  halfpm6th  8143  2halves  8152  halfaddsub  8157  avglt1  8161  avglt2  8162  div4p1lem1div2  8175  nneoor  8338  zeo  8341  divlt1lt  8648  divle1le  8649  2tnp1ge0ge0  9141  frecfzennn  9201  expge1  9290  cjreb  9464  sqrt2gt1lt2  9645  amgm2  9712  ex-an  9892  ex-fl  9893  bdbm1.3ii  10009
  Copyright terms: Public domain W3C validator