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  557  biijust  641  3pm3.2i  1175  sbequilem  1838  unssi  3311  ssini  3359  bm1.3ii  4125  epelg  4291  pwnex  4450  onsucelsucexmid  4530  elvv  4689  funpr  5269  mpov  5965  caovcom  6032  th3q  6640  endisj  6824  phplem2  6853  addnnnq0  7448  mulnnnq0  7449  nqprxx  7545  addsrpr  7744  mulsrpr  7745  recidpirq  7857  apreim  8560  aptap  8607  mulcanapi  8624  div1  8660  recdivap  8675  divdivap1  8680  divdivap2  8681  divassapi  8725  divdirapi  8726  div23api  8727  div11api  8728  divmuldivapi  8729  divmul13api  8730  divadddivapi  8731  divdivdivapi  8732  lemulge11  8823  negiso  8912  2cnne0  9128  2rene0  9129  1mhlfehlf  9137  halfpm6th  9139  2halves  9148  halfaddsub  9153  avglt1  9157  avglt2  9158  div4p1lem1div2  9172  3halfnz  9350  nneoor  9355  zeo  9358  divlt1lt  9724  divle1le  9725  nnledivrp  9766  fz0to4untppr  10124  2tnp1ge0ge0  10301  frecfzennn  10426  fxnn0nninf  10438  expge1  10557  faclbnd2  10722  4bc2eq6  10754  cjreb  10875  sqrt2gt1lt2  11058  amgm2  11127  xrnegiso  11270  ege2le3  11679  efi4p  11725  efival  11740  cosmul  11753  sin01bnd  11765  cos01bnd  11766  cos1bnd  11767  cos2bnd  11768  sin01gt0  11769  cos01gt0  11770  sin02gt0  11771  sincos2sgn  11773  sin4lt0  11774  egt2lt3  11787  3dvdsdec  11870  3dvds2dec  11871  odd2np1  11878  oddge22np1  11886  ltoddhalfle  11898  halfleoddlt  11899  nno  11911  ndvdsi  11938  flodddiv4  11939  flodddiv4lt  11941  flodddiv4t2lthalf  11942  3lcm2e6woprm  12086  6lcm4e12  12087  pcrec  12308  ennnfonelemj0  12402  structfn  12481  ndxslid  12487  strleun  12563  slotsdifipndx  12633  slotsdifplendx  12665  slotsdifdsndx  12676  slotsdifunifndx  12683  cnfld1  13469  isbasis3g  13549  bl2in  13906  dveflem  14190  cosz12  14204  sinhalfpilem  14215  ptolemy  14248  sincosq1lem  14249  sincosq4sgn  14253  sinq12gt0  14254  cosq23lt0  14257  coseq00topi  14259  coseq0negpitopi  14260  tangtx  14262  sincos4thpi  14264  sincos6thpi  14266  sincos3rdpi  14267  pigt3  14268  coskpi  14272  cos02pilt1  14275  2logb9irrALT  14395  lgsdir2lem1  14432  1lgs  14447  2lgsoddprmlem1  14456  ex-an  14478  ex-fl  14480  ex-exp  14482  bdbm1.3ii  14646  subctctexmid  14753