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  424  pm4.87  547  biijust  631  3pm3.2i  1160  sbequilem  1811  unssi  3256  ssini  3304  bm1.3ii  4057  epelg  4220  pwnex  4378  onsucelsucexmid  4453  elvv  4609  funpr  5183  mpov  5869  caovcom  5936  th3q  6542  endisj  6726  phplem2  6755  addnnnq0  7281  mulnnnq0  7282  nqprxx  7378  addsrpr  7577  mulsrpr  7578  recidpirq  7690  apreim  8389  mulcanapi  8452  div1  8487  recdivap  8502  divdivap1  8507  divdivap2  8508  divassapi  8552  divdirapi  8553  div23api  8554  div11api  8555  divmuldivapi  8556  divmul13api  8557  divadddivapi  8558  divdivdivapi  8559  lemulge11  8648  negiso  8737  2cnne0  8953  2rene0  8954  1mhlfehlf  8962  halfpm6th  8964  2halves  8973  halfaddsub  8978  avglt1  8982  avglt2  8983  div4p1lem1div2  8997  3halfnz  9172  nneoor  9177  zeo  9180  divlt1lt  9541  divle1le  9542  nnledivrp  9583  2tnp1ge0ge0  10105  frecfzennn  10230  fxnn0nninf  10242  expge1  10361  faclbnd2  10520  4bc2eq6  10552  cjreb  10670  sqrt2gt1lt2  10853  amgm2  10922  xrnegiso  11063  ege2le3  11414  efi4p  11460  efival  11475  cosmul  11488  sin01bnd  11500  cos01bnd  11501  cos1bnd  11502  cos2bnd  11503  sin01gt0  11504  cos01gt0  11505  sin02gt0  11506  sincos2sgn  11508  sin4lt0  11509  egt2lt3  11522  3dvdsdec  11598  3dvds2dec  11599  odd2np1  11606  oddge22np1  11614  ltoddhalfle  11626  halfleoddlt  11627  nno  11639  ndvdsi  11666  flodddiv4  11667  flodddiv4lt  11669  flodddiv4t2lthalf  11670  3lcm2e6woprm  11803  6lcm4e12  11804  ennnfonelemj0  11950  structfn  12017  ndxslid  12023  strleun  12087  isbasis3g  12252  bl2in  12611  dveflem  12895  cosz12  12909  sinhalfpilem  12920  ptolemy  12953  sincosq1lem  12954  sincosq4sgn  12958  sinq12gt0  12959  cosq23lt0  12962  coseq00topi  12964  coseq0negpitopi  12965  tangtx  12967  sincos4thpi  12969  sincos6thpi  12971  sincos3rdpi  12972  pigt3  12973  coskpi  12977  cos02pilt1  12980  2logb9irrALT  13099  ex-an  13106  ex-fl  13108  ex-exp  13110  bdbm1.3ii  13260  subctctexmid  13369