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  1178  sbequilem  1862  unssi  3352  ssini  3400  bm1.3ii  4173  epelg  4345  pwnex  4504  onsucelsucexmid  4586  elvv  4745  relopabiv  4809  funpr  5335  mpov  6048  caovcom  6117  th3q  6740  endisj  6934  phplem2  6965  addnnnq0  7582  mulnnnq0  7583  nqprxx  7679  addsrpr  7878  mulsrpr  7879  recidpirq  7991  apreim  8696  aptap  8743  mulcanapi  8760  div1  8796  recdivap  8811  divdivap1  8816  divdivap2  8817  divassapi  8861  divdirapi  8862  div23api  8863  div11api  8864  divmuldivapi  8865  divmul13api  8866  divadddivapi  8867  divdivdivapi  8868  lemulge11  8959  negiso  9048  2cnne0  9266  2rene0  9267  1mhlfehlf  9275  halfpm6th  9277  2halves  9286  halfaddsub  9291  avglt1  9296  avglt2  9297  div4p1lem1div2  9311  3halfnz  9490  nneoor  9495  zeo  9498  divlt1lt  9866  divle1le  9867  nnledivrp  9908  fz0to4untppr  10266  2tnp1ge0ge0  10466  frecfzennn  10593  xnn0nnen  10604  fxnn0nninf  10606  expge1  10743  faclbnd2  10909  4bc2eq6  10941  cjreb  11252  sqrt2gt1lt2  11435  amgm2  11504  xrnegiso  11648  ege2le3  12057  efi4p  12103  efival  12118  cosmul  12131  sin01bnd  12143  cos01bnd  12144  cos1bnd  12145  cos2bnd  12146  sin01gt0  12148  cos01gt0  12149  sin02gt0  12150  sincos2sgn  12152  sin4lt0  12153  egt2lt3  12166  3dvdsdec  12251  3dvds2dec  12252  odd2np1  12259  oddge22np1  12267  ltoddhalfle  12279  halfleoddlt  12280  nno  12292  ndvdsi  12319  flodddiv4  12322  flodddiv4lt  12324  flodddiv4t2lthalf  12325  bitsp1o  12339  3lcm2e6woprm  12483  6lcm4e12  12484  pcrec  12706  ennnfonelemj0  12847  structfn  12926  ndxslid  12932  strleun  13011  slotsdifipndx  13082  slotsdifplendx  13117  slotsdifdsndx  13132  slotsdifunifndx  13139  cnfld1  14409  expghmap  14444  isbasis3g  14593  bl2in  14950  dveflem  15273  cosz12  15327  sinhalfpilem  15338  ptolemy  15371  sincosq1lem  15372  sincosq4sgn  15376  sinq12gt0  15377  cosq23lt0  15380  coseq00topi  15382  coseq0negpitopi  15383  tangtx  15385  sincos4thpi  15387  sincos6thpi  15389  sincos3rdpi  15390  pigt3  15391  coskpi  15395  cos02pilt1  15398  2logb9irrALT  15521  lgsdir2lem1  15580  1lgs  15595  gausslemma2dlem0c  15603  gausslemma2dlem0d  15604  gausslemma2dlem1a  15610  gausslemma2dlem2  15614  gausslemma2dlem3  15615  lgsquad2lem2  15634  2lgslem1a1  15638  2lgslem1a2  15639  2lgslem1c  15642  2lgslem3  15653  2lgsoddprmlem1  15657  ex-an  15798  ex-fl  15800  ex-exp  15802  bdbm1.3ii  15965  subctctexmid  16078