Theorem pm3.2i 471

Description: Infer conjunction of premises. (Contributed by NM, 21-Jun-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 463	. 2 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
4	1, 2, 3	mp2 9	1 |- ( ph /\ ps )

Syntax hints:   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  pm4.87  608  dfbi  661  mp4an  709  3pm3.2i  1239  unssi  3788  ssini  3836  bm1.3ii  4784  epelg  5030  elvv  5177  relopabi  5245  funpr  5944  funcnvpr  5950  mpt2v  6750  caovcom  6831  snnex  6966  pwnex  6968  1st2val  7194  2nd2val  7195  elxp7  7201  mptmpt2opabbrd  7248  wfrlem13  7427  wfr3  7435  tfr1a  7490  oeoa  7677  oeoe  7679  erov  7844  endisj  8047  phplem2  8140  snopfsupp  8298  r1funlim  8629  dfac2  8953  cflecard  9075  canth4  9469  canthnumlem  9470  canthwelem  9472  canthp1lem2  9475  pwfseqlem4  9484  wunex3  9563  addsrpr  9896  mulsrpr  9897  recexsrlem  9924  mulcani  10666  div1  10716  recdiv  10731  divdiv1  10736  divdiv2  10737  div23i  10783  div11i  10784  divmuldivi  10785  divadddivi  10787  divdivdivi  10788  lemulge11  10885  negiso  11003  dfnn3  11034  2cnne0  11242  2rene0  11243  halfpm6th  11253  avglt1  11270  avglt2  11271  div4p1lem1div2  11287  3halfnz  11456  divlt1lt  11899  divle1le  11900  nnledivrp  11940  x2times  12129  xrsupsslem  12137  xrinfmsslem  12138  fz0to4untppr  12442  fldiv4lem1div2uz2  12637  om2uzoi  12754  fzennn  12767  expge1  12897  sqoddm1div8  13028  faclbnd2  13078  faclbnd4lem1  13080  4bc2eq6  13116  hashfxnn0  13124  hashfOLD  13126  hashsnlei  13206  hashunlei  13212  hashsslei  13213  hash2prb  13254  repswccat  13532  cshwsexa  13570  funcnvs4  13660  f1oun2prg  13662  wrdlen2i  13686  relexpaddg  13793  cjreb  13863  sqrt2gt1lt2  14015  abs1m  14075  amgm2  14109  climcndslem2  14582  fprodn0f  14722  bpoly3  14789  efcllem  14808  ege2le3  14820  efi4p  14867  efival  14882  sin01bnd  14915  cos01bnd  14916  cos1bnd  14917  cos2bnd  14918  sin01gt0  14920  cos01gt0  14921  sin02gt0  14922  sincos2sgn  14924  sin4lt0  14925  egt2lt3  14934  rpnnen2lem3  14945  rpnnen2lem11  14953  nthruc  14981  nthruz  14982  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  mod2eq1n2dvds  15071  oddge22np1  15073  halfleoddlt  15086  nno  15098  divalglem5  15120  ndvdsi  15136  flodddiv4  15137  flodddiv4lt  15139  flodddiv4t2lthalf  15140  bitsp1o  15155  3lcm2e6woprm  15328  6lcm4e12  15329  pcrec  15563  prmrec  15626  prmo1  15741  prmgaplcmlem1  15755  prmgaplcm  15764  modsubi  15776  structfn  15874  strlemor0OLD  15968  strlemor1OLD  15969  strleun  15972  isofn  16435  sscres  16483  funcestrcsetclem7  16786  funcestrcsetclem8  16787  fullestrcsetc  16791  mgmnsgrpex  17418  ga0  17731  symg2bas  17818  f1otrspeq  17867  psgnsn  17940  0frgp  18192  gsummptnn0fz  18382  srgbinomlem4  18543  psrbag0  19494  psrbagsn  19495  coe1fsupp  19584  coe1mul2  19639  evls1sca  19688  cnfldfun  19758  cnfldfunALT  19759  cnfld1  19771  cnsubdrglem  19797  expmhm  19815  expghm  19844  matmulr  20244  mat1dimelbas  20277  mat1f1o  20284  m2detleib  20437  smadiadetglem1  20477  pmatcollpw3fi1lem2  20592  cpmidpmatlem2  20676  cpmadumatpolylem1  20686  cayhamlem3  20692  cayhamlem4  20693  toprntopon  20729  isbasis3g  20753  fctop  20808  cctop  20810  refref  21316  bl2in  22205  dscmet  22377  iihalf1  22730  iihalf2  22732  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  iscvsi  22929  zclmncvs  22948  ncvs1  22957  minveclem2  23197  minveclem4  23203  ovolunlem1a  23264  volf  23297  i1f1lem  23456  mbfi1fseqlem5  23486  dveflem  23742  pilem2  24206  pilem3  24207  sinhalfpilem  24215  sincosq1lem  24249  tangtx  24257  sinq12gt0  24259  sincos4thpi  24265  sincos6thpi  24267  sincos3rdpi  24268  pige3  24269  coseq1  24274  efeq1  24275  efif1olem4  24291  logblog  24530  angneg  24533  ang180lem1  24539  1cubrlem  24568  quart1  24583  log2cnv  24671  log2tlbnd  24672  log2ublem1  24673  log2ub  24676  emcllem1  24722  emcllem6  24727  basellem1  24807  basellem2  24808  basellem3  24809  basellem8  24814  ppiublem1  24927  ppiublem2  24928  ppiub  24929  chtublem  24936  chtub  24937  bcmono  25002  bclbnd  25005  bpos1lem  25007  bposlem1  25009  bposlem2  25010  bposlem3  25011  bposlem4  25012  bposlem5  25013  bposlem6  25014  bposlem7  25015  bposlem8  25016  bposlem9  25017  lgsdir2lem1  25050  1lgs  25065  gausslemma2dlem0c  25083  gausslemma2dlem0d  25084  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  gausslemma2dlem3  25093  gausslemma2dlem5  25096  gausslemma2dlem6  25097  lgsquad2lem2  25110  2lgslem1a1  25114  2lgslem1a2  25115  2lgslem1c  25118  2lgslem3a  25121  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2lgslem3  25129  2lgsoddprmlem1  25133  chebbnd1lem1  25158  chebbnd1lem3  25160  chebbnd1  25161  dchrisum0flblem2  25198  dchrisum0lem1  25205  mulog2sumlem2  25224  selberglem2  25235  chpdifbndlem1  25242  ercgrg  25412  axlowdimlem4  25825  axlowdimlem5  25826  axlowdimlem6  25827  axlowdimlem7  25828  axlowdimlem8  25829  axlowdimlem10  25831  axlowdimlem11  25832  graop  25921  grastruct  25922  uhgrunop  25970  upgrop  25989  upgrunop  26014  umgrunop  26016  usgrop  26058  usgr2v1e2w  26144  usgrexmpldifpr  26150  usgrexmpledg  26154  uhgrsubgrself  26172  uhgrspan1lem1  26192  upgrres1lem1  26201  fusgrfis  26222  vtxd0nedgb  26384  p1evtxdeqlem  26408  p1evtxdeq  26409  p1evtxdp1  26410  umgr2v2e  26421  vdegp1bi  26433  wlkcomp  26526  upgr2pthnlp  26628  usgr2trlncl  26656  usgr2pthlem  26659  clwlkcomp  26675  uspgrn2crct  26700  wspthnonp  26744  2wlkond  26833  2pthond  26838  2pthon3v  26839  umgr2adedgwlkonALT  26843  umgr2wlk  26845  umgr2wlkon  26846  wpthswwlks2on  26854  elwspths2spth  26862  0ewlk  26975  0pth  26986  0pthonv  26990  1pthon2v  27013  3wlkdlem4  27022  3trlond  27033  3pthond  27035  3spthond  27037  trlsegvdeglem3  27082  eupthvdres  27095  eupth2lemb  27097  ex-natded5.2i  27263  ex-an  27279  ex-id  27291  ex-po  27292  ex-fl  27304  ex-mod  27306  ex-exp  27307  ex-lcm  27315  nvz0  27523  ipidsq  27565  ipdirilem  27684  siilem1  27706  minvecolem2  27731  minvecolem3  27732  minvecolem4  27736  hvsubcan  27931  hvsubcan2  27932  normlem7tALT  27976  helch  28100  hsn0elch  28105  hhshsslem2  28125  hhsssh  28126  shscli  28176  shintcli  28188  shintcl  28189  chintcli  28190  chintcl  28191  shincli  28221  shsval2i  28246  omlsi  28263  chincli  28319  chabs1  28375  fh1i  28480  fh2i  28481  cm2ji  28484  pjnormi  28580  nmopsetn0  28724  nmfnsetn0  28737  lnophm  28878  nmcexi  28885  nmbdfnlb  28909  imaelshi  28917  nlelshi  28919  nmopadjlem  28948  nmopcoadji  28960  hmopidmch  29012  hmopidmpj  29013  sto1i  29095  stlei  29099  stji1i  29101  csmdsymi  29193  chirred  29254  cdj3lem1  29293  rpdp2cl  29589  dp2lt10  29591  dp2lt  29592  dp2ltc  29594  dpfrac1  29599  dpfrac1OLD  29600  dplti  29613  dpgti  29614  dpexpp1  29616  dpadd3  29620  dpmul  29621  dpmul4  29622  xrsclat  29680  nn0archi  29843  lmatfvlem  29881  xrge0iifmhm  29985  qqh0  30028  qqh1  30029  rerrext  30053  cnrrext  30054  prsiga  30194  oms0  30359  coinfliprv  30544  ballotlem1  30548  ballotth  30599  signsw0g  30633  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  hgt750leme  30736  tgoldbachgt  30741  subfacval2  31169  erdszelem2  31174  cvmliftlem4  31270  elmrsubrn  31417  msubfval  31421  problem4  31562  quad3  31564  dfpo2  31645  br6  31647  dfon2lem3  31690  poseq  31750  fullfunfnv  32053  fneref  32345  filnetlem2  32374  filnetlem3  32375  onpsstopbas  32429  dnizeq0  32465  dnibndlem12  32479  knoppcnlem5  32487  knoppcnlem8  32490  knoppcnlem10  32492  knoppcnlem11  32493  knoppndvlem14  32516  cnndvlem1  32528  bj-genr  32591  bj-genl  32592  bj-genan  32593  bj-2upln1upl  33012  bj-vtoclgfALT  33021  taupilem1  33167  topdifinf  33197  sin2h  33399  cos2h  33400  tan2h  33401  pigt3  33402  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem29  33438  poimirlem31  33440  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnclem2  33462  asindmre  33495  heiborlem7  33616  riscer  33787  ac6s6f  33981  ishlatiN  34642  0psubN  35035  atpsubN  35039  mzpclall  37290  diophin  37336  diophun  37337  eldioph4b  37375  irrapx1  37392  2nn0ind  37510  aomclem4  37627  ifpid3g  37837  ifpid2g  37838  ifpbi1b  37848  pwinfi  37869  rtrclex  37924  cnvrcl0  37932  dfrcl2  37966  relexp1idm  38006  relexp0idm  38007  clsk1independent  38344  lhe4.4ex1a  38528  expgrowth  38534  ax6e2nd  38774  uun0.1  39005  relopabVD  39137  ax6e2ndVD  39144  sb5ALTVD  39149  ax6e2ndALT  39166  fnchoice  39188  limsuppnfdlem  39933  dvmptconst  40129  dvmptidg  40131  dvmulcncf  40140  dvdivcncf  40142  dvnprodlem3  40163  itgsinexplem1  40169  volioof  40204  stoweidlem13  40230  stoweidlem14  40231  stoweidlem26  40243  stoweidlem34  40251  stoweidlem49  40266  stoweidlem59  40276  dirkertrigeqlem3  40317  dirkercncflem1  40320  dirkercncflem2  40321  fourierdlem57  40380  fourierdlem62  40385  fourierdlem103  40426  fourierdlem111  40434  fourierswlem  40447  fouriersw  40448  salexct2  40557  salexct3  40560  salgencntex  40561  salgensscntex  40562  gsumge0cl  40588  sge00  40593  sge0tsms  40597  0ome  40743  ovnlecvr  40772  ovn0lem  40779  hoidmvle  40814  ovnsubadd2lem  40859  smflimlem6  40984  mbfpsssmf  40991  smfmullem4  41001  smfpimbor1lem1  41005  astbstanbst  41076  aistbistaandb  41077  abnotataxb  41083  aifftbifffaibif  41088  confun4  41109  plcofph  41111  plvcofph  41113  plvcofphax  41114  plvofpos  41115  mdandyv0  41116  mdandyv1  41117  mdandyv2  41118  mdandyv3  41119  mdandyv4  41120  mdandyv5  41121  mdandyv6  41122  mdandyv7  41123  mdandyv8  41124  mdandyv9  41125  mdandyv10  41126  mdandyv11  41127  mdandyv12  41128  mdandyv13  41129  mdandyv14  41130  mdandyv15  41131  mdandyvr0  41132  mdandyvr1  41133  mdandyvr2  41134  mdandyvr3  41135  mdandyvr4  41136  mdandyvr5  41137  mdandyvr6  41138  mdandyvr7  41139  mdandyvrx0  41148  mdandyvrx1  41149  mdandyvrx2  41150  mdandyvrx3  41151  mdandyvrx4  41152  mdandyvrx5  41153  mdandyvrx6  41154  mdandyvrx7  41155  dandysum2p2e4  41165  dfnelbr2  41290  pfx2  41412  fmtno4prmfac  41484  31prm  41512  lighneallem4a  41525  41prothprmlem2  41535  zofldiv2ALTV  41574  gbegt5  41649  gbowgt5  41650  gboge9  41652  9gbo  41662  11gbo  41663  nnsum3primes4  41676  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  tgblthelfgott  41703  tgoldbach  41705  tgblthelfgottOLD  41709  tgoldbachOLD  41712  mgmplusgiopALT  41830  sgrp2sgrp  41864  isrnghm  41892  2zrngaabl  41944  rnghmsscmap2  41973  rnghmsscmap  41974  funcrngcsetc  41998  funcrngcsetcALT  41999  rhmsscmap2  42019  rhmsscmap  42020  funcringcsetc  42035  funcringcsetcALTV2lem8  42043  funcringcsetclem8ALTV  42066  zlmodzxzlmod  42132  zlmodzxzel  42133  zlmodzxzscm  42135  zlmodzxzadd  42136  snlindsntorlem  42259  ldepspr  42262  lmod1lem2  42277  lmod1lem3  42278  lmod1lem4  42279  lmod1lem5  42280  lmodn0  42284  zlmodzxznm  42286  zlmodzxzldeplem  42287  zlmodzxzldeplem1  42289  zlmodzxzldeplem3  42291  lvecpsslmod  42296  ldepsnlinc  42297  ldepslinc  42298  expnegico01  42308  zofldiv2  42325  flnn0div2ge  42327  elbigo2  42346  nnlog2ge0lt1  42360  digfval  42391  dignnld  42397  dignn0flhalf  42412  alimp-surprise  42526  aacllem  42547