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  8933  aptap  8980  mulcanapi  8997  div1  9035  recdivap  9050  divdivap1  9055  divdivap2  9056  divassapi  9100  divdirapi  9101  div23api  9102  div11api  9103  divmuldivapi  9104  divmul13api  9105  divadddivapi  9106  divdivdivapi  9107  lemulge11  9198  negiso  9287  2cnne0  9518  2rene0  9519  1mhlfehlf  9527  halfpm6th  9529  2halves  9538  halfaddsub  9543  avglt1  9548  avglt2  9549  div4p1lem1div2  9563  3halfnz  9747  nneoor  9752  zeo  9755  divlt1lt  10135  divle1le  10136  nnledivrp  10177  fz0to4untppr  10541  2tnp1ge0ge0  10749  frecfzennn  10876  xnn0nnen  10887  fxnn0nninf  10889  expge1  11026  faclbnd2  11194  4bc2eq6  11227  cjreb  11645  sqrt2gt1lt2  11829  amgm2  11899  xrnegiso  12044  ege2le3  12454  efi4p  12500  efival  12515  cosmul  12528  sin01bnd  12540  cos01bnd  12541  cos1bnd  12542  cos2bnd  12543  sin01gt0  12545  cos01gt0  12546  sin02gt0  12547  sincos2sgn  12549  sin4lt0  12550  egt2lt3  12563  3dvdsdec  12648  3dvds2dec  12649  odd2np1  12656  oddge22np1  12664  ltoddhalfle  12676  halfleoddlt  12677  nno  12689  ndvdsi  12716  flodddiv4  12719  flodddiv4lt  12721  flodddiv4t2lthalf  12722  bitsp1o  12736  3lcm2e6woprm  12880  6lcm4e12  12881  pcrec  13107  ballotfilemonn  13270  ballotfilemth  13330  ennnfonelemj0  13341  structfn  13420  ndxslid  13426  strleun  13507  slotsdifipndx  13578  slotsdifplendx  13613  slotsdifdsndx  13628  slotsdifunifndx  13635  cnfld1  14958  expghmap  14991  isbasis3g  15196  bl2in  15553  dveflem  15876  cosz12  15931  sinhalfpilem  15942  ptolemy  15975  sincosq1lem  15976  sincosq4sgn  15980  sinq12gt0  15981  cosq23lt0  15984  coseq00topi  15986  coseq0negpitopi  15987  tangtx  15989  sincos4thpi  15991  sincos6thpi  15993  sincos3rdpi  15994  pigt3  15995  coskpi  15999  cos02pilt1  16002  2logb9irrALT  16129  log2tlbndlog2  16139  log2ublem1  16140  log2ublog2  16143  ppiublem1  16192  ppiublem2  16193  ppiqub  16194  bcmono  16202  bclbnd  16205  bpos1lem  16207  bposlem1  16209  bposlem2  16210  bposlem3  16211  bposlem4  16212  bposlem5  16213  lgsdir2lem1  16245  1lgs  16260  gausslemma2dlem0c  16268  gausslemma2dlem0d  16269  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  gausslemma2dlem3  16280  lgsquad2lem2  16299  2lgslem1a1  16303  2lgslem1a2  16304  2lgslem1c  16307  2lgslem3  16318  2lgsoddprmlem1  16322  usgrexmpldifpr  16588  uhgrsubgrself  16605  konigsberglem1  16827  ex-an  16835  ex-fl  16837  ex-exp  16839  bdbm1.3ii  17015  subctctexmid  17128  wexmiddifxy  17144  qdiff  17196