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  559  biijust  646  3pm3.2i  1202  sbequilem  1887  unssi  3396  ssini  3446  bm1.3ii  4233  epelg  4413  pwnex  4572  onsucelsucexmid  4654  elvv  4814  relopabiv  4880  funpr  5410  mpov  6145  caovcom  6214  th3q  6876  endisj  7077  phplem2  7109  ssfiexmidt  7135  addnnnq0  7766  mulnnnq0  7767  nqprxx  7863  addsrpr  8062  mulsrpr  8063  recidpirq  8175  apreim  8879  aptap  8926  mulcanapi  8943  div1  8979  recdivap  8994  divdivap1  8999  divdivap2  9000  divassapi  9044  divdirapi  9045  div23api  9046  div11api  9047  divmuldivapi  9048  divmul13api  9049  divadddivapi  9050  divdivdivapi  9051  lemulge11  9142  negiso  9231  2cnne0  9449  2rene0  9450  1mhlfehlf  9458  halfpm6th  9460  2halves  9469  halfaddsub  9474  avglt1  9479  avglt2  9480  div4p1lem1div2  9494  3halfnz  9678  nneoor  9683  zeo  9686  divlt1lt  10060  divle1le  10061  nnledivrp  10102  fz0to4untppr  10462  2tnp1ge0ge0  10665  frecfzennn  10792  xnn0nnen  10803  fxnn0nninf  10805  expge1  10942  faclbnd2  11108  4bc2eq6  11141  cjreb  11555  sqrt2gt1lt2  11738  amgm2  11807  xrnegiso  11951  ege2le3  12361  efi4p  12407  efival  12422  cosmul  12435  sin01bnd  12447  cos01bnd  12448  cos1bnd  12449  cos2bnd  12450  sin01gt0  12452  cos01gt0  12453  sin02gt0  12454  sincos2sgn  12456  sin4lt0  12457  egt2lt3  12470  3dvdsdec  12555  3dvds2dec  12556  odd2np1  12563  oddge22np1  12571  ltoddhalfle  12583  halfleoddlt  12584  nno  12596  ndvdsi  12623  flodddiv4  12626  flodddiv4lt  12628  flodddiv4t2lthalf  12629  bitsp1o  12643  3lcm2e6woprm  12787  6lcm4e12  12788  pcrec  13010  ballotfilemonn  13144  ennnfonelemj0  13169  structfn  13248  ndxslid  13254  strleun  13334  slotsdifipndx  13405  slotsdifplendx  13440  slotsdifdsndx  13455  slotsdifunifndx  13462  cnfld1  14737  expghmap  14772  isbasis3g  14928  bl2in  15285  dveflem  15608  cosz12  15662  sinhalfpilem  15673  ptolemy  15706  sincosq1lem  15707  sincosq4sgn  15711  sinq12gt0  15712  cosq23lt0  15715  coseq00topi  15717  coseq0negpitopi  15718  tangtx  15720  sincos4thpi  15722  sincos6thpi  15724  sincos3rdpi  15725  pigt3  15726  coskpi  15730  cos02pilt1  15733  2logb9irrALT  15856  lgsdir2lem1  15918  1lgs  15933  gausslemma2dlem0c  15941  gausslemma2dlem0d  15942  gausslemma2dlem1a  15948  gausslemma2dlem2  15952  gausslemma2dlem3  15953  lgsquad2lem2  15972  2lgslem1a1  15976  2lgslem1a2  15977  2lgslem1c  15980  2lgslem3  15991  2lgsoddprmlem1  15995  usgrexmpldifpr  16261  uhgrsubgrself  16278  konigsberglem1  16500  ex-an  16508  ex-fl  16510  ex-exp  16512  bdbm1.3ii  16678  subctctexmid  16791  qdiff  16850