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  4256  epelg  4437  pwnex  4597  onsucelsucexmid  4679  elvv  4839  relopabiv  4905  funpr  5436  mpov  6181  caovcom  6250  th3q  6919  endisj  7128  phplem2  7160  ssfiexmidt  7186  addnnnq0  7822  mulnnnq0  7823  nqprxx  7919  addsrpr  8118  mulsrpr  8119  recidpirq  8231  apreim  8939  aptap  8986  mulcanapi  9003  div1  9041  recdivap  9056  divdivap1  9061  divdivap2  9062  divassapi  9106  divdirapi  9107  div23api  9108  div11api  9109  divmuldivapi  9110  divmul13api  9111  divadddivapi  9112  divdivdivapi  9113  lemulge11  9204  negiso  9293  2cnne0  9525  2rene0  9526  1mhlfehlf  9534  halfpm6th  9536  2halves  9545  halfaddsub  9550  avglt1  9555  avglt2  9556  div4p1lem1div2  9570  3halfnz  9753  nneoor  9758  zeo  9761  divlt1lt  10141  divle1le  10142  nnledivrp  10183  fz0to4untppr  10547  2tnp1ge0ge0  10756  frecfzennn  10883  xnn0nnen  10894  fxnn0nninf  10896  expge1  11033  faclbnd2  11201  4bc2eq6  11234  cjreb  11652  sqrt2gt1lt2  11836  amgm2  11906  xrnegiso  12052  ege2le3  12462  efi4p  12508  efival  12523  cosmul  12536  sin01bnd  12548  cos01bnd  12549  cos1bnd  12550  cos2bnd  12551  sin01gt0  12553  cos01gt0  12554  sin02gt0  12555  sincos2sgn  12557  sin4lt0  12558  egt2lt3  12571  3dvdsdec  12656  3dvds2dec  12657  odd2np1  12664  oddge22np1  12672  ltoddhalfle  12684  halfleoddlt  12685  nno  12697  ndvdsi  12724  flodddiv4  12727  flodddiv4lt  12729  flodddiv4t2lthalf  12730  bitsp1o  12744  3lcm2e6woprm  12888  6lcm4e12  12889  pcrec  13115  ballotfilemonn  13278  ballotfilemth  13338  ennnfonelemj0  13349  structfn  13428  ndxslid  13434  strleun  13516  slotsdifipndx  13587  slotsdifplendx  13622  slotsdifdsndx  13637  slotsdifunifndx  13644  cnfld1  15017  expghmap  15050  isbasis3g  15289  bl2in  15646  dveflem  15969  cosz12  16024  sinhalfpilem  16035  ptolemy  16068  sincosq1lem  16069  sincosq4sgn  16073  sinq12gt0  16074  cosq23lt0  16077  coseq00topi  16079  coseq0negpitopi  16080  tangtx  16082  sincos4thpi  16084  sincos6thpi  16086  sincos3rdpi  16087  pigt3  16088  coskpi  16092  cos02pilt1  16096  2logb9irrALT  16227  log2tlbndlog2  16237  log2ublem1  16238  log2ublog2  16241  ppiublem1  16308  ppiublem2  16309  ppiqub  16310  chtublem  16312  chtqub  16313  bcmono  16321  bclbnd  16324  bpos1lem  16326  bposlem1  16328  bposlem2  16329  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem7  16334  bposlem8  16335  bposlem9  16336  lgsdir2lem1  16369  1lgs  16384  gausslemma2dlem0c  16392  gausslemma2dlem0d  16393  gausslemma2dlem1a  16399  gausslemma2dlem2  16403  gausslemma2dlem3  16404  lgsquad2lem2  16423  2lgslem1a1  16427  2lgslem1a2  16428  2lgslem1c  16431  2lgslem3  16442  2lgsoddprmlem1  16446  usgrexmpldifpr  16712  uhgrsubgrself  16729  konigsberglem1  16951  ex-an  16959  ex-fl  16961  ex-exp  16963  bdbm1.3ii  17139  subctctexmid  17252  wexmiddifxy  17268  qdiff  17322