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 )

Syntax hints:   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mp4an  427  pm4.87  559  biijust  646  3pm3.2i  1201  sbequilem  1886  unssi  3382  ssini  3430  bm1.3ii  4210  epelg  4387  pwnex  4546  onsucelsucexmid  4628  elvv  4788  relopabiv  4853  funpr  5382  mpov  6110  caovcom  6179  th3q  6808  endisj  7007  phplem2  7038  ssfiexmidt  7064  addnnnq0  7668  mulnnnq0  7669  nqprxx  7765  addsrpr  7964  mulsrpr  7965  recidpirq  8077  apreim  8782  aptap  8829  mulcanapi  8846  div1  8882  recdivap  8897  divdivap1  8902  divdivap2  8903  divassapi  8947  divdirapi  8948  div23api  8949  div11api  8950  divmuldivapi  8951  divmul13api  8952  divadddivapi  8953  divdivdivapi  8954  lemulge11  9045  negiso  9134  2cnne0  9352  2rene0  9353  1mhlfehlf  9361  halfpm6th  9363  2halves  9372  halfaddsub  9377  avglt1  9382  avglt2  9383  div4p1lem1div2  9397  3halfnz  9576  nneoor  9581  zeo  9584  divlt1lt  9958  divle1le  9959  nnledivrp  10000  fz0to4untppr  10358  2tnp1ge0ge0  10560  frecfzennn  10687  xnn0nnen  10698  fxnn0nninf  10700  expge1  10837  faclbnd2  11003  4bc2eq6  11035  cjreb  11426  sqrt2gt1lt2  11609  amgm2  11678  xrnegiso  11822  ege2le3  12231  efi4p  12277  efival  12292  cosmul  12305  sin01bnd  12317  cos01bnd  12318  cos1bnd  12319  cos2bnd  12320  sin01gt0  12322  cos01gt0  12323  sin02gt0  12324  sincos2sgn  12326  sin4lt0  12327  egt2lt3  12340  3dvdsdec  12425  3dvds2dec  12426  odd2np1  12433  oddge22np1  12441  ltoddhalfle  12453  halfleoddlt  12454  nno  12466  ndvdsi  12493  flodddiv4  12496  flodddiv4lt  12498  flodddiv4t2lthalf  12499  bitsp1o  12513  3lcm2e6woprm  12657  6lcm4e12  12658  pcrec  12880  ennnfonelemj0  13021  structfn  13100  ndxslid  13106  strleun  13186  slotsdifipndx  13257  slotsdifplendx  13292  slotsdifdsndx  13307  slotsdifunifndx  13314  cnfld1  14585  expghmap  14620  isbasis3g  14769  bl2in  15126  dveflem  15449  cosz12  15503  sinhalfpilem  15514  ptolemy  15547  sincosq1lem  15548  sincosq4sgn  15552  sinq12gt0  15553  cosq23lt0  15556  coseq00topi  15558  coseq0negpitopi  15559  tangtx  15561  sincos4thpi  15563  sincos6thpi  15565  sincos3rdpi  15566  pigt3  15567  coskpi  15571  cos02pilt1  15574  2logb9irrALT  15697  lgsdir2lem1  15756  1lgs  15771  gausslemma2dlem0c  15779  gausslemma2dlem0d  15780  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  gausslemma2dlem3  15791  lgsquad2lem2  15810  2lgslem1a1  15814  2lgslem1a2  15815  2lgslem1c  15818  2lgslem3  15829  2lgsoddprmlem1  15833  usgrexmpldifpr  16099  uhgrsubgrself  16116  ex-an  16319  ex-fl  16321  ex-exp  16323  bdbm1.3ii  16486  subctctexmid  16601