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

Theorem pm3.2i 270
Description: Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
pm3.2i.1  |-  ph
pm3.2i.2  |-  ps
Assertion
Ref Expression
pm3.2i  |-  ( ph  /\ 
ps )

Proof of Theorem pm3.2i
StepHypRef Expression
1 pm3.2i.1 . 2  |-  ph
2 pm3.2i.2 . 2  |-  ps
3 pm3.2 138 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
41, 2, 3mp2 16 1  |-  ( ph  /\ 
ps )
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  546  biijust  630  3pm3.2i  1159  sbequilem  1810  unssi  3251  ssini  3299  bm1.3ii  4049  epelg  4212  pwnex  4370  onsucelsucexmid  4445  elvv  4601  funpr  5175  mpov  5861  caovcom  5928  th3q  6534  endisj  6718  phplem2  6747  addnnnq0  7264  mulnnnq0  7265  nqprxx  7361  addsrpr  7560  mulsrpr  7561  recidpirq  7673  apreim  8372  mulcanapi  8435  div1  8470  recdivap  8485  divdivap1  8490  divdivap2  8491  divassapi  8535  divdirapi  8536  div23api  8537  div11api  8538  divmuldivapi  8539  divmul13api  8540  divadddivapi  8541  divdivdivapi  8542  lemulge11  8631  negiso  8720  2cnne0  8936  2rene0  8937  1mhlfehlf  8945  halfpm6th  8947  2halves  8956  halfaddsub  8961  avglt1  8965  avglt2  8966  div4p1lem1div2  8980  3halfnz  9155  nneoor  9160  zeo  9163  divlt1lt  9518  divle1le  9519  nnledivrp  9560  2tnp1ge0ge0  10081  frecfzennn  10206  fxnn0nninf  10218  expge1  10337  faclbnd2  10495  4bc2eq6  10527  cjreb  10645  sqrt2gt1lt2  10828  amgm2  10897  xrnegiso  11038  ege2le3  11384  efi4p  11430  efival  11445  cosmul  11458  sin01bnd  11470  cos01bnd  11471  cos1bnd  11472  cos2bnd  11473  sin01gt0  11474  cos01gt0  11475  sin02gt0  11476  sincos2sgn  11478  sin4lt0  11479  egt2lt3  11492  3dvdsdec  11568  3dvds2dec  11569  odd2np1  11576  oddge22np1  11584  ltoddhalfle  11596  halfleoddlt  11597  nno  11609  ndvdsi  11636  flodddiv4  11637  flodddiv4lt  11639  flodddiv4t2lthalf  11640  3lcm2e6woprm  11773  6lcm4e12  11774  ennnfonelemj0  11920  structfn  11987  ndxslid  11993  strleun  12057  isbasis3g  12222  bl2in  12581  dveflem  12864  cosz12  12877  sinhalfpilem  12888  ptolemy  12921  sincosq1lem  12922  sincosq4sgn  12926  sinq12gt0  12927  cosq23lt0  12930  coseq00topi  12932  coseq0negpitopi  12933  tangtx  12935  sincos4thpi  12937  sincos6thpi  12939  sincos3rdpi  12940  pigt3  12941  coskpi  12945  cos02pilt1  12948  ex-an  12988  ex-fl  12990  ex-exp  12992  bdbm1.3ii  13142  subctctexmid  13249
  Copyright terms: Public domain W3C validator