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  424  pm4.87  547  biijust  631  3pm3.2i  1160  sbequilem  1811  unssi  3255  ssini  3303  bm1.3ii  4056  epelg  4219  pwnex  4377  onsucelsucexmid  4452  elvv  4608  funpr  5182  mpov  5868  caovcom  5935  th3q  6541  endisj  6725  phplem2  6754  addnnnq0  7280  mulnnnq0  7281  nqprxx  7377  addsrpr  7576  mulsrpr  7577  recidpirq  7689  apreim  8388  mulcanapi  8451  div1  8486  recdivap  8501  divdivap1  8506  divdivap2  8507  divassapi  8551  divdirapi  8552  div23api  8553  div11api  8554  divmuldivapi  8555  divmul13api  8556  divadddivapi  8557  divdivdivapi  8558  lemulge11  8647  negiso  8736  2cnne0  8952  2rene0  8953  1mhlfehlf  8961  halfpm6th  8963  2halves  8972  halfaddsub  8977  avglt1  8981  avglt2  8982  div4p1lem1div2  8996  3halfnz  9171  nneoor  9176  zeo  9179  divlt1lt  9540  divle1le  9541  nnledivrp  9582  2tnp1ge0ge0  10104  frecfzennn  10229  fxnn0nninf  10241  expge1  10360  faclbnd2  10519  4bc2eq6  10551  cjreb  10669  sqrt2gt1lt2  10852  amgm2  10921  xrnegiso  11062  ege2le3  11412  efi4p  11458  efival  11473  cosmul  11486  sin01bnd  11498  cos01bnd  11499  cos1bnd  11500  cos2bnd  11501  sin01gt0  11502  cos01gt0  11503  sin02gt0  11504  sincos2sgn  11506  sin4lt0  11507  egt2lt3  11520  3dvdsdec  11596  3dvds2dec  11597  odd2np1  11604  oddge22np1  11612  ltoddhalfle  11624  halfleoddlt  11625  nno  11637  ndvdsi  11664  flodddiv4  11665  flodddiv4lt  11667  flodddiv4t2lthalf  11668  3lcm2e6woprm  11801  6lcm4e12  11802  ennnfonelemj0  11948  structfn  12015  ndxslid  12021  strleun  12085  isbasis3g  12250  bl2in  12609  dveflem  12893  cosz12  12907  sinhalfpilem  12918  ptolemy  12951  sincosq1lem  12952  sincosq4sgn  12956  sinq12gt0  12957  cosq23lt0  12960  coseq00topi  12962  coseq0negpitopi  12963  tangtx  12965  sincos4thpi  12967  sincos6thpi  12969  sincos3rdpi  12970  pigt3  12971  coskpi  12975  cos02pilt1  12978  2logb9irrALT  13097  ex-an  13104  ex-fl  13106  ex-exp  13108  bdbm1.3ii  13258  subctctexmid  13367
  Copyright terms: Public domain W3C validator