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  642  3pm3.2i  1177  sbequilem  1860  unssi  3347  ssini  3395  bm1.3ii  4164  epelg  4336  pwnex  4495  onsucelsucexmid  4577  elvv  4736  relopabiv  4800  funpr  5325  mpov  6034  caovcom  6103  th3q  6726  endisj  6918  phplem2  6949  addnnnq0  7561  mulnnnq0  7562  nqprxx  7658  addsrpr  7857  mulsrpr  7858  recidpirq  7970  apreim  8675  aptap  8722  mulcanapi  8739  div1  8775  recdivap  8790  divdivap1  8795  divdivap2  8796  divassapi  8840  divdirapi  8841  div23api  8842  div11api  8843  divmuldivapi  8844  divmul13api  8845  divadddivapi  8846  divdivdivapi  8847  lemulge11  8938  negiso  9027  2cnne0  9245  2rene0  9246  1mhlfehlf  9254  halfpm6th  9256  2halves  9265  halfaddsub  9270  avglt1  9275  avglt2  9276  div4p1lem1div2  9290  3halfnz  9469  nneoor  9474  zeo  9477  divlt1lt  9845  divle1le  9846  nnledivrp  9887  fz0to4untppr  10245  2tnp1ge0ge0  10442  frecfzennn  10569  xnn0nnen  10580  fxnn0nninf  10582  expge1  10719  faclbnd2  10885  4bc2eq6  10917  cjreb  11119  sqrt2gt1lt2  11302  amgm2  11371  xrnegiso  11515  ege2le3  11924  efi4p  11970  efival  11985  cosmul  11998  sin01bnd  12010  cos01bnd  12011  cos1bnd  12012  cos2bnd  12013  sin01gt0  12015  cos01gt0  12016  sin02gt0  12017  sincos2sgn  12019  sin4lt0  12020  egt2lt3  12033  3dvdsdec  12118  3dvds2dec  12119  odd2np1  12126  oddge22np1  12134  ltoddhalfle  12146  halfleoddlt  12147  nno  12159  ndvdsi  12186  flodddiv4  12189  flodddiv4lt  12191  flodddiv4t2lthalf  12192  bitsp1o  12206  3lcm2e6woprm  12350  6lcm4e12  12351  pcrec  12573  ennnfonelemj0  12714  structfn  12793  ndxslid  12799  strleun  12878  slotsdifipndx  12949  slotsdifplendx  12984  slotsdifdsndx  12999  slotsdifunifndx  13006  cnfld1  14276  expghmap  14311  isbasis3g  14460  bl2in  14817  dveflem  15140  cosz12  15194  sinhalfpilem  15205  ptolemy  15238  sincosq1lem  15239  sincosq4sgn  15243  sinq12gt0  15244  cosq23lt0  15247  coseq00topi  15249  coseq0negpitopi  15250  tangtx  15252  sincos4thpi  15254  sincos6thpi  15256  sincos3rdpi  15257  pigt3  15258  coskpi  15262  cos02pilt1  15265  2logb9irrALT  15388  lgsdir2lem1  15447  1lgs  15462  gausslemma2dlem0c  15470  gausslemma2dlem0d  15471  gausslemma2dlem1a  15477  gausslemma2dlem2  15481  gausslemma2dlem3  15482  lgsquad2lem2  15501  2lgslem1a1  15505  2lgslem1a2  15506  2lgslem1c  15509  2lgslem3  15520  2lgsoddprmlem1  15524  ex-an  15592  ex-fl  15594  ex-exp  15596  bdbm1.3ii  15760  subctctexmid  15870