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

Step	Hyp	Ref	Expression
1		pm3.2i.1	. 2 |- ph
2		pm3.2i.2	. 2 |- ps
3		pm3.2 138	. 2 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
4	1, 2, 3	mp2 16	1 |- ( ph /\ ps )

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  425  pm4.87  552  biijust  636  3pm3.2i  1170  sbequilem  1831  unssi  3302  ssini  3350  bm1.3ii  4110  epelg  4275  pwnex  4434  onsucelsucexmid  4514  elvv  4673  funpr  5250  mpov  5943  caovcom  6010  th3q  6618  endisj  6802  phplem2  6831  addnnnq0  7411  mulnnnq0  7412  nqprxx  7508  addsrpr  7707  mulsrpr  7708  recidpirq  7820  apreim  8522  mulcanapi  8585  div1  8620  recdivap  8635  divdivap1  8640  divdivap2  8641  divassapi  8685  divdirapi  8686  div23api  8687  div11api  8688  divmuldivapi  8689  divmul13api  8690  divadddivapi  8691  divdivdivapi  8692  lemulge11  8782  negiso  8871  2cnne0  9087  2rene0  9088  1mhlfehlf  9096  halfpm6th  9098  2halves  9107  halfaddsub  9112  avglt1  9116  avglt2  9117  div4p1lem1div2  9131  3halfnz  9309  nneoor  9314  zeo  9317  divlt1lt  9681  divle1le  9682  nnledivrp  9723  fz0to4untppr  10080  2tnp1ge0ge0  10257  frecfzennn  10382  fxnn0nninf  10394  expge1  10513  faclbnd2  10676  4bc2eq6  10708  cjreb  10830  sqrt2gt1lt2  11013  amgm2  11082  xrnegiso  11225  ege2le3  11634  efi4p  11680  efival  11695  cosmul  11708  sin01bnd  11720  cos01bnd  11721  cos1bnd  11722  cos2bnd  11723  sin01gt0  11724  cos01gt0  11725  sin02gt0  11726  sincos2sgn  11728  sin4lt0  11729  egt2lt3  11742  3dvdsdec  11824  3dvds2dec  11825  odd2np1  11832  oddge22np1  11840  ltoddhalfle  11852  halfleoddlt  11853  nno  11865  ndvdsi  11892  flodddiv4  11893  flodddiv4lt  11895  flodddiv4t2lthalf  11896  3lcm2e6woprm  12040  6lcm4e12  12041  pcrec  12262  ennnfonelemj0  12356  structfn  12435  ndxslid  12441  strleun  12507  isbasis3g  12838  bl2in  13197  dveflem  13481  cosz12  13495  sinhalfpilem  13506  ptolemy  13539  sincosq1lem  13540  sincosq4sgn  13544  sinq12gt0  13545  cosq23lt0  13548  coseq00topi  13550  coseq0negpitopi  13551  tangtx  13553  sincos4thpi  13555  sincos6thpi  13557  sincos3rdpi  13558  pigt3  13559  coskpi  13563  cos02pilt1  13566  2logb9irrALT  13686  lgsdir2lem1  13723  1lgs  13738  ex-an  13758  ex-fl  13760  ex-exp  13762  bdbm1.3ii  13926  subctctexmid  14034