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  7816  mulnnnq0  7817  nqprxx  7913  addsrpr  8112  mulsrpr  8113  recidpirq  8225  apreim  8931  aptap  8978  mulcanapi  8995  div1  9033  recdivap  9048  divdivap1  9053  divdivap2  9054  divassapi  9098  divdirapi  9099  div23api  9100  div11api  9101  divmuldivapi  9102  divmul13api  9103  divadddivapi  9104  divdivdivapi  9105  lemulge11  9196  negiso  9285  2cnne0  9514  2rene0  9515  1mhlfehlf  9523  halfpm6th  9525  2halves  9534  halfaddsub  9539  avglt1  9544  avglt2  9545  div4p1lem1div2  9559  3halfnz  9743  nneoor  9748  zeo  9751  divlt1lt  10125  divle1le  10126  nnledivrp  10167  fz0to4untppr  10531  2tnp1ge0ge0  10736  frecfzennn  10863  xnn0nnen  10874  fxnn0nninf  10876  expge1  11013  faclbnd2  11180  4bc2eq6  11213  cjreb  11631  sqrt2gt1lt2  11815  amgm2  11884  xrnegiso  12028  ege2le3  12438  efi4p  12484  efival  12499  cosmul  12512  sin01bnd  12524  cos01bnd  12525  cos1bnd  12526  cos2bnd  12527  sin01gt0  12529  cos01gt0  12530  sin02gt0  12531  sincos2sgn  12533  sin4lt0  12534  egt2lt3  12547  3dvdsdec  12632  3dvds2dec  12633  odd2np1  12640  oddge22np1  12648  ltoddhalfle  12660  halfleoddlt  12661  nno  12673  ndvdsi  12700  flodddiv4  12703  flodddiv4lt  12705  flodddiv4t2lthalf  12706  bitsp1o  12720  3lcm2e6woprm  12864  6lcm4e12  12865  pcrec  13087  ballotfilemonn  13221  ballotfilemth  13281  ennnfonelemj0  13292  structfn  13371  ndxslid  13377  strleun  13458  slotsdifipndx  13529  slotsdifplendx  13564  slotsdifdsndx  13579  slotsdifunifndx  13586  cnfld1  14909  expghmap  14942  isbasis3g  15147  bl2in  15504  dveflem  15827  cosz12  15881  sinhalfpilem  15892  ptolemy  15925  sincosq1lem  15926  sincosq4sgn  15930  sinq12gt0  15931  cosq23lt0  15934  coseq00topi  15936  coseq0negpitopi  15937  tangtx  15939  sincos4thpi  15941  sincos6thpi  15943  sincos3rdpi  15944  pigt3  15945  coskpi  15949  cos02pilt1  15952  2logb9irrALT  16076  log2tlbndlog2  16082  log2ublem1  16083  log2ublog2  16086  lgsdir2lem1  16147  1lgs  16162  gausslemma2dlem0c  16170  gausslemma2dlem0d  16171  gausslemma2dlem1a  16177  gausslemma2dlem2  16181  gausslemma2dlem3  16182  lgsquad2lem2  16201  2lgslem1a1  16205  2lgslem1a2  16206  2lgslem1c  16209  2lgslem3  16220  2lgsoddprmlem1  16224  usgrexmpldifpr  16490  uhgrsubgrself  16507  konigsberglem1  16729  ex-an  16737  ex-fl  16739  ex-exp  16741  bdbm1.3ii  16917  subctctexmid  17030  wexmiddifxy  17046  qdiff  17098