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  6918  endisj  7126  phplem2  7158  ssfiexmidt  7184  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  9754  nneoor  9759  zeo  9762  divlt1lt  10142  divle1le  10143  nnledivrp  10184  fz0to4untppr  10548  2tnp1ge0ge0  10757  frecfzennn  10884  xnn0nnen  10895  fxnn0nninf  10897  expge1  11034  faclbnd2  11202  4bc2eq6  11235  cjreb  11653  sqrt2gt1lt2  11837  amgm2  11907  xrnegiso  12053  ege2le3  12463  efi4p  12509  efival  12524  cosmul  12537  sin01bnd  12549  cos01bnd  12550  cos1bnd  12551  cos2bnd  12552  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  sincos2sgn  12558  sin4lt0  12559  egt2lt3  12572  3dvdsdec  12657  3dvds2dec  12658  odd2np1  12665  oddge22np1  12673  ltoddhalfle  12685  halfleoddlt  12686  nno  12698  ndvdsi  12725  flodddiv4  12728  flodddiv4lt  12730  flodddiv4t2lthalf  12731  bitsp1o  12745  3lcm2e6woprm  12889  6lcm4e12  12890  pcrec  13116  ballotfilemonn  13279  ballotfilemth  13339  ennnfonelemj0  13350  structfn  13429  ndxslid  13435  strleun  13517  slotsdifipndx  13588  slotsdifplendx  13623  slotsdifdsndx  13638  slotsdifunifndx  13645  cnfld1  15018  expghmap  15051  isbasis3g  15272  bl2in  15629  dveflem  15952  cosz12  16007  sinhalfpilem  16018  ptolemy  16051  sincosq1lem  16052  sincosq4sgn  16056  sinq12gt0  16057  cosq23lt0  16060  coseq00topi  16062  coseq0negpitopi  16063  tangtx  16065  sincos4thpi  16067  sincos6thpi  16069  sincos3rdpi  16070  pigt3  16071  coskpi  16075  cos02pilt1  16079  2logb9irrALT  16210  log2tlbndlog2  16220  log2ublem1  16221  log2ublog2  16224  ppiublem1  16291  ppiublem2  16292  ppiqub  16293  chtublem  16295  chtqub  16296  bcmono  16304  bclbnd  16307  bpos1lem  16309  bposlem1  16311  bposlem2  16312  bposlem3  16313  bposlem4  16314  bposlem5  16315  bposlem6  16316  bposlem7  16317  bposlem8  16318  bposlem9  16319  lgsdir2lem1  16352  1lgs  16367  gausslemma2dlem0c  16375  gausslemma2dlem0d  16376  gausslemma2dlem1a  16382  gausslemma2dlem2  16386  gausslemma2dlem3  16387  lgsquad2lem2  16406  2lgslem1a1  16410  2lgslem1a2  16411  2lgslem1c  16414  2lgslem3  16425  2lgsoddprmlem1  16429  usgrexmpldifpr  16695  uhgrsubgrself  16712  konigsberglem1  16934  ex-an  16942  ex-fl  16944  ex-exp  16946  bdbm1.3ii  17122  subctctexmid  17235  wexmiddifxy  17251  qdiff  17305