Theorem pm3.2i 272

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 139	. 2 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
4	1, 2, 3	mp2 16	1 |- ( ph /\ ps )

This proof depends on syntax axioms:   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mp4an  431  pm4.87  563  biijust  650  3pm3.2i  1206  sbequilem  1891  unssi  3404  ssini  3454  bm1.3ii  4254  epelg  4435  pwnex  4595  onsucelsucexmid  4677  elvv  4837  relopabiv  4903  funpr  5433  mpov  6178  caovcom  6247  th3q  6914  endisj  7122  phplem2  7154  ssfiexmidt  7180  addnnnq0  7817  mulnnnq0  7818  nqprxx  7914  addsrpr  8113  mulsrpr  8114  recidpirq  8226  apreim  8934  aptap  8981  mulcanapi  8998  div1  9036  recdivap  9051  divdivap1  9056  divdivap2  9057  divassapi  9101  divdirapi  9102  div23api  9103  div11api  9104  divmuldivapi  9105  divmul13api  9106  divadddivapi  9107  divdivdivapi  9108  lemulge11  9199  negiso  9288  2cnne0  9519  2rene0  9520  1mhlfehlf  9528  halfpm6th  9530  2halves  9539  halfaddsub  9544  avglt1  9549  avglt2  9550  div4p1lem1div2  9564  3halfnz  9748  nneoor  9753  zeo  9756  divlt1lt  10136  divle1le  10137  nnledivrp  10178  fz0to4untppr  10542  2tnp1ge0ge0  10751  frecfzennn  10878  xnn0nnen  10889  fxnn0nninf  10891  expge1  11028  faclbnd2  11196  4bc2eq6  11229  cjreb  11647  sqrt2gt1lt2  11831  amgm2  11901  xrnegiso  12047  ege2le3  12457  efi4p  12503  efival  12518  cosmul  12531  sin01bnd  12543  cos01bnd  12544  cos1bnd  12545  cos2bnd  12546  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  sincos2sgn  12552  sin4lt0  12553  egt2lt3  12566  3dvdsdec  12651  3dvds2dec  12652  odd2np1  12659  oddge22np1  12667  ltoddhalfle  12679  halfleoddlt  12680  nno  12692  ndvdsi  12719  flodddiv4  12722  flodddiv4lt  12724  flodddiv4t2lthalf  12725  bitsp1o  12739  3lcm2e6woprm  12883  6lcm4e12  12884  pcrec  13110  ballotfilemonn  13273  ballotfilemth  13333  ennnfonelemj0  13344  structfn  13423  ndxslid  13429  strleun  13511  slotsdifipndx  13582  slotsdifplendx  13617  slotsdifdsndx  13632  slotsdifunifndx  13639  cnfld1  14993  expghmap  15026  isbasis3g  15238  bl2in  15595  dveflem  15918  cosz12  15973  sinhalfpilem  15984  ptolemy  16017  sincosq1lem  16018  sincosq4sgn  16022  sinq12gt0  16023  cosq23lt0  16026  coseq00topi  16028  coseq0negpitopi  16029  tangtx  16031  sincos4thpi  16033  sincos6thpi  16035  sincos3rdpi  16036  pigt3  16037  coskpi  16041  cos02pilt1  16044  2logb9irrALT  16171  log2tlbndlog2  16181  log2ublem1  16182  log2ublog2  16185  ppiublem1  16252  ppiublem2  16253  ppiqub  16254  chtublem  16256  chtqub  16257  bcmono  16265  bclbnd  16268  bpos1lem  16270  bposlem1  16272  bposlem2  16273  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  bposlem7  16278  bposlem8  16279  bposlem9  16280  lgsdir2lem1  16313  1lgs  16328  gausslemma2dlem0c  16336  gausslemma2dlem0d  16337  gausslemma2dlem1a  16343  gausslemma2dlem2  16347  gausslemma2dlem3  16348  lgsquad2lem2  16367  2lgslem1a1  16371  2lgslem1a2  16372  2lgslem1c  16375  2lgslem3  16386  2lgsoddprmlem1  16390  usgrexmpldifpr  16656  uhgrsubgrself  16673  konigsberglem1  16895  ex-an  16903  ex-fl  16905  ex-exp  16907  bdbm1.3ii  17083  subctctexmid  17196  wexmiddifxy  17212  qdiff  17265