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  3310  ssini  3358  bm1.3ii  4124  epelg  4290  pwnex  4449  onsucelsucexmid  4529  elvv  4688  funpr  5268  mpov  5964  caovcom  6031  th3q  6639  endisj  6823  phplem2  6852  addnnnq0  7447  mulnnnq0  7448  nqprxx  7544  addsrpr  7743  mulsrpr  7744  recidpirq  7856  apreim  8559  aptap  8606  mulcanapi  8623  div1  8659  recdivap  8674  divdivap1  8679  divdivap2  8680  divassapi  8724  divdirapi  8725  div23api  8726  div11api  8727  divmuldivapi  8728  divmul13api  8729  divadddivapi  8730  divdivdivapi  8731  lemulge11  8822  negiso  8911  2cnne0  9127  2rene0  9128  1mhlfehlf  9136  halfpm6th  9138  2halves  9147  halfaddsub  9152  avglt1  9156  avglt2  9157  div4p1lem1div2  9171  3halfnz  9349  nneoor  9354  zeo  9357  divlt1lt  9723  divle1le  9724  nnledivrp  9765  fz0to4untppr  10123  2tnp1ge0ge0  10300  frecfzennn  10425  fxnn0nninf  10437  expge1  10556  faclbnd2  10721  4bc2eq6  10753  cjreb  10874  sqrt2gt1lt2  11057  amgm2  11126  xrnegiso  11269  ege2le3  11678  efi4p  11724  efival  11739  cosmul  11752  sin01bnd  11764  cos01bnd  11765  cos1bnd  11766  cos2bnd  11767  sin01gt0  11768  cos01gt0  11769  sin02gt0  11770  sincos2sgn  11772  sin4lt0  11773  egt2lt3  11786  3dvdsdec  11869  3dvds2dec  11870  odd2np1  11877  oddge22np1  11885  ltoddhalfle  11897  halfleoddlt  11898  nno  11910  ndvdsi  11937  flodddiv4  11938  flodddiv4lt  11940  flodddiv4t2lthalf  11941  3lcm2e6woprm  12085  6lcm4e12  12086  pcrec  12307  ennnfonelemj0  12401  structfn  12480  ndxslid  12486  strleun  12562  slotsdifipndx  12632  slotsdifplendx  12664  slotsdifdsndx  12675  slotsdifunifndx  12682  cnfld1  13436  isbasis3g  13516  bl2in  13873  dveflem  14157  cosz12  14171  sinhalfpilem  14182  ptolemy  14215  sincosq1lem  14216  sincosq4sgn  14220  sinq12gt0  14221  cosq23lt0  14224  coseq00topi  14226  coseq0negpitopi  14227  tangtx  14229  sincos4thpi  14231  sincos6thpi  14233  sincos3rdpi  14234  pigt3  14235  coskpi  14239  cos02pilt1  14242  2logb9irrALT  14362  lgsdir2lem1  14399  1lgs  14414  2lgsoddprmlem1  14423  ex-an  14445  ex-fl  14447  ex-exp  14449  bdbm1.3ii  14613  subctctexmid  14720