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  1849  unssi  3334  ssini  3382  bm1.3ii  4150  epelg  4321  pwnex  4480  onsucelsucexmid  4562  elvv  4721  relopabiv  4785  funpr  5306  mpov  6008  caovcom  6076  th3q  6694  endisj  6878  phplem2  6909  addnnnq0  7509  mulnnnq0  7510  nqprxx  7606  addsrpr  7805  mulsrpr  7806  recidpirq  7918  apreim  8622  aptap  8669  mulcanapi  8686  div1  8722  recdivap  8737  divdivap1  8742  divdivap2  8743  divassapi  8787  divdirapi  8788  div23api  8789  div11api  8790  divmuldivapi  8791  divmul13api  8792  divadddivapi  8793  divdivdivapi  8794  lemulge11  8885  negiso  8974  2cnne0  9191  2rene0  9192  1mhlfehlf  9200  halfpm6th  9202  2halves  9211  halfaddsub  9216  avglt1  9221  avglt2  9222  div4p1lem1div2  9236  3halfnz  9414  nneoor  9419  zeo  9422  divlt1lt  9790  divle1le  9791  nnledivrp  9832  fz0to4untppr  10190  2tnp1ge0ge0  10370  frecfzennn  10497  xnn0nnen  10508  fxnn0nninf  10510  expge1  10647  faclbnd2  10813  4bc2eq6  10845  cjreb  11010  sqrt2gt1lt2  11193  amgm2  11262  xrnegiso  11405  ege2le3  11814  efi4p  11860  efival  11875  cosmul  11888  sin01bnd  11900  cos01bnd  11901  cos1bnd  11902  cos2bnd  11903  sin01gt0  11905  cos01gt0  11906  sin02gt0  11907  sincos2sgn  11909  sin4lt0  11910  egt2lt3  11923  3dvdsdec  12006  3dvds2dec  12007  odd2np1  12014  oddge22np1  12022  ltoddhalfle  12034  halfleoddlt  12035  nno  12047  ndvdsi  12074  flodddiv4  12075  flodddiv4lt  12077  flodddiv4t2lthalf  12078  3lcm2e6woprm  12224  6lcm4e12  12225  pcrec  12446  ennnfonelemj0  12558  structfn  12637  ndxslid  12643  strleun  12722  slotsdifipndx  12792  slotsdifplendx  12827  slotsdifdsndx  12838  slotsdifunifndx  12845  cnfld1  14060  expghmap  14095  isbasis3g  14214  bl2in  14571  dveflem  14872  cosz12  14915  sinhalfpilem  14926  ptolemy  14959  sincosq1lem  14960  sincosq4sgn  14964  sinq12gt0  14965  cosq23lt0  14968  coseq00topi  14970  coseq0negpitopi  14971  tangtx  14973  sincos4thpi  14975  sincos6thpi  14977  sincos3rdpi  14978  pigt3  14979  coskpi  14983  cos02pilt1  14986  2logb9irrALT  15106  lgsdir2lem1  15144  1lgs  15159  gausslemma2dlem0c  15167  gausslemma2dlem0d  15168  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  gausslemma2dlem3  15179  2lgsoddprmlem1  15193  ex-an  15215  ex-fl  15217  ex-exp  15219  bdbm1.3ii  15383  subctctexmid  15491