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

Theorem pm3.2i 270
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 138 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
41, 2, 3mp2 16 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  mp4an  423  pm4.87  531  biijust  615  3pm3.2i  1144  sbequilem  1794  unssi  3221  ssini  3269  bm1.3ii  4019  epelg  4182  pwnex  4340  onsucelsucexmid  4415  elvv  4571  funpr  5145  mpov  5829  caovcom  5896  th3q  6502  endisj  6686  phplem2  6715  addnnnq0  7225  mulnnnq0  7226  nqprxx  7322  addsrpr  7521  mulsrpr  7522  recidpirq  7634  apreim  8333  mulcanapi  8396  div1  8431  recdivap  8446  divdivap1  8451  divdivap2  8452  divassapi  8496  divdirapi  8497  div23api  8498  div11api  8499  divmuldivapi  8500  divmul13api  8501  divadddivapi  8502  divdivdivapi  8503  lemulge11  8592  negiso  8681  2cnne0  8897  2rene0  8898  1mhlfehlf  8906  halfpm6th  8908  2halves  8917  halfaddsub  8922  avglt1  8926  avglt2  8927  div4p1lem1div2  8941  3halfnz  9116  nneoor  9121  zeo  9124  divlt1lt  9479  divle1le  9480  nnledivrp  9521  2tnp1ge0ge0  10042  frecfzennn  10167  fxnn0nninf  10179  expge1  10298  faclbnd2  10456  4bc2eq6  10488  cjreb  10606  sqrt2gt1lt2  10789  amgm2  10858  xrnegiso  10999  ege2le3  11304  efi4p  11351  efival  11366  cosmul  11379  sin01bnd  11391  cos01bnd  11392  cos1bnd  11393  cos2bnd  11394  sin01gt0  11395  cos01gt0  11396  sin02gt0  11397  sincos2sgn  11399  sin4lt0  11400  egt2lt3  11413  3dvdsdec  11489  3dvds2dec  11490  odd2np1  11497  oddge22np1  11505  ltoddhalfle  11517  halfleoddlt  11518  nno  11530  ndvdsi  11557  flodddiv4  11558  flodddiv4lt  11560  flodddiv4t2lthalf  11561  3lcm2e6woprm  11694  6lcm4e12  11695  ennnfonelemj0  11841  structfn  11905  ndxslid  11911  strleun  11975  isbasis3g  12140  bl2in  12499  dveflem  12782  cosz12  12788  sinhalfpilem  12799  ptolemy  12832  sincosq1lem  12833  sincosq4sgn  12837  sinq12gt0  12838  cosq23lt0  12841  coseq00topi  12843  coseq0negpitopi  12844  tangtx  12846  sincos4thpi  12848  sincos6thpi  12850  sincos3rdpi  12851  pigt3  12852  coskpi  12856  cos02pilt1  12859  ex-an  12862  ex-fl  12864  ex-exp  12866  bdbm1.3ii  13016  subctctexmid  13123
  Copyright terms: Public domain W3C validator