Theorem pm3.2i 471

Description: Infer conjunction of premises. Inference associated with pm3.2 470. Its associated deduction is jca 516 (and the double deduction is jcad 517). (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
pm3.2i.1	⊢ 𝜑
pm3.2i.2	⊢ 𝜓

Assertion

Ref	Expression
pm3.2i	⊢ (𝜑 ∧ 𝜓)

Proof of Theorem pm3.2i

Step	Hyp	Ref	Expression
1		pm3.2i.1	. 2 ⊢ 𝜑
2		pm3.2i.2	. 2 ⊢ 𝜓
3		pm3.2 470	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
4	1, 2, 3	mp2 9	1 ⊢ (𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mp4an  699  pm4.87  849  3pm3.2i  1346  unssi  4127  ssini  4175  opthhausdorff  5465  elvv  5700  elopaelxp  5715  relopabiv  5770  relopabi  5772  dfpo2  6254  funpr  6548  funcnvpr  6554  mpov  7475  caovcom  7560  snnex  7708  pwnex  7709  1st2val  7966  2nd2val  7967  elxp7  7973  opreuopreu  7983  poxp2  8090  poseq  8105  tfr1a  8330  oeoa  8530  oeoe  8532  erov  8758  endisj  8999  snopfsupp  9301  ssttrcl  9634  ttrclselem2  9645  r1funlim  9688  dfac2b  10051  cflecard  10173  canth4  10568  canthnumlem  10569  canthwelem  10571  canthp1lem2  10574  pwfseqlem4  10583  wunex3  10662  addsrpr  10996  mulsrpr  10997  recexsrlem  11024  mulcani  11787  div1  11842  recdiv  11859  divdiv1  11864  divdiv2  11865  div23i  11911  div11i  11912  divmuldivi  11913  divadddivi  11915  divdivdivi  11916  lemulge11  12016  negiso  12134  dfnn3  12186  2cnne0  12384  2rene0  12385  halfpm6th  12397  avglt1  12413  avglt2  12414  div4p1lem1div2  12430  3halfnz  12606  divlt1lt  13011  divle1le  13012  nnledivrp  13054  x2times  13249  xrsupsslem  13257  xrinfmsslem  13258  nnge2recico01  13458  fvf1tp  13746  om2uzoi  13915  fzennn  13928  expge1  14059  sqoddm1div8  14203  faclbnd2  14251  faclbnd4lem1  14253  4bc2eq6  14289  hashfxnn0  14297  hashsnlei  14378  hashunlei  14385  hashsslei  14386  hash2prb  14432  repswccat  14746  funcnvs4  14875  f1oun2prg  14877  wrdlen2i  14902  s2rn  14923  s3rn  14924  s7rn  14925  relexpaddg  15013  cjreb  15083  sqrt2gt1lt2  15234  abs1m  15296  bpoly3  16021  ege2le3  16053  efi4p  16102  efival  16117  sin01bnd  16150  cos01bnd  16151  cos1bnd  16152  cos2bnd  16153  sin01gt0  16155  cos01gt0  16156  sin02gt0  16157  sincos2sgn  16159  sin4lt0  16160  egt2lt3  16171  rpnnen2lem3  16181  rpnnen2lem11  16189  nthruc  16217  nthruz  16218  3dvdsdec  16299  3dvds2dec  16300  mod2eq1n2dvds  16314  halfleoddlt  16329  divalglem5  16364  ndvdsi  16379  flodddiv4  16382  flodddiv4lt  16384  bitsp1o  16400  3lcm2e6woprm  16582  6lcm4e12  16583  pcrec  16827  prmrec  16891  prmgaplcmlem1  17020  prmgaplcm  17029  modsubi  17041  structfn  17124  strleun  17125  slotsdifipndx  17296  slotsdifplendx  17336  slotsdifdsndx  17355  slotsdifunifndx  17362  slotsdifplendx2  17377  slotsdifocndx  17378  isofn  17740  sscres  17788  funcestrcsetclem7  18110  funcestrcsetclem8  18111  fullestrcsetc  18115  nulchn  18583  chninf  18599  mgmnsgrpex  18900  pwmnd  18906  ga0  19271  symg2bas  19366  f1otrspeq  19420  psgnsn  19493  0frgp  19752  gsummptnn0fz  19959  srgbinomlem4  20208  isrnghm  20419  rnghmsscmap2  20608  rnghmsscmap  20609  funcrngcsetc  20619  funcrngcsetcALT  20620  rhmsscmap2  20637  rhmsscmap  20638  funcringcsetc  20653  cnfldfun  21368  cnfldfunALT  21369  cnfld1  21379  cnsubdrglem  21400  expmhm  21418  expghm  21457  pzriprnglem4  21466  pzriprnglem9  21471  pzriprnglem14  21476  pzriprng1ALT  21478  psrbag0  22045  psrbagsn  22046  coe1fsupp  22206  coe1mul2  22262  evls1sca  22316  matmulr  22428  mat1dimelbas  22461  mat1f1o  22468  m2detleib  22621  smadiadetglem1  22661  pmatcollpw3fi1lem2  22777  cpmidpmatlem2  22861  cpmadumatpolylem1  22871  cayhamlem3  22877  cayhamlem4  22878  isbasis3g  22939  fctop  22994  cctop  22996  refref  23503  bl2in  24390  dscmet  24562  iihalf1  24923  iihalf2  24925  icopnfhmeo  24935  iccpnfhmeo  24937  xrhmeo  24938  iscvsi  25121  zclmncvs  25140  ncvs1  25149  ehl2eudis  25414  minveclem2  25418  minveclem4  25424  ovolunlem1a  25488  volf  25521  i1f1lem  25681  mbfi1fseqlem5  25711  dveflem  25971  pilem2  26442  pilem3  26443  sinhalfpilem  26452  sincosq1lem  26486  tangtx  26494  sinq12gt0  26496  sincos4thpi  26502  sincos6thpi  26505  sincos3rdpi  26506  pigt3  26507  pige3ALT  26509  coseq1  26514  efeq1  26517  efif1olem4  26534  angneg  26792  ang180lem1  26798  1cubrlem  26830  quart1  26845  log2cnv  26933  log2tlbnd  26934  log2ublem1  26935  log2ub  26938  emcllem1  26984  emcllem6  26989  basellem1  27069  basellem2  27070  basellem3  27071  basellem8  27076  ppiublem1  27190  ppiublem2  27191  ppiub  27192  chtublem  27199  chtub  27200  bcmono  27265  bclbnd  27268  bpos1lem  27270  bposlem1  27272  bposlem2  27273  bposlem3  27274  bposlem4  27275  bposlem5  27276  bposlem6  27277  bposlem7  27278  bposlem8  27279  bposlem9  27280  lgsdir2lem1  27313  1lgs  27328  gausslemma2dlem0c  27346  gausslemma2dlem0d  27347  gausslemma2dlem1a  27353  gausslemma2dlem2  27355  gausslemma2dlem3  27356  gausslemma2dlem5  27359  gausslemma2dlem6  27360  lgsquad2lem2  27373  2lgslem1a1  27377  2lgslem1a2  27378  2lgslem1c  27381  2lgslem3a  27384  2lgslem3b  27385  2lgslem3c  27386  2lgslem3d  27387  2lgslem3  27392  2lgsoddprmlem1  27396  addsqrexnreu  27430  addsqnreup  27431  chebbnd1lem1  27457  chebbnd1lem3  27459  chebbnd1  27460  dchrisum0flblem2  27497  dchrisum0lem1  27504  mulog2sumlem2  27523  selberglem2  27534  chpdifbndlem1  27541  sltssnb  27786  mulscl  28151  ltmuls  28153  divs1  28221  precsexlem8  28231  0reno  28513  1reno  28514  slotsinbpsd  28534  slotslnbpsd  28535  ercgrg  28610  axlowdimlem4  29039  axlowdimlem5  29040  axlowdimlem6  29041  axlowdimlem7  29042  axlowdimlem8  29043  axlowdimlem10  29045  axlowdimlem11  29046  graop  29123  grastruct  29124  uhgrunop  29169  upgrop  29188  upgrunop  29213  umgrunop  29215  usgrop  29257  usgr2v1e2w  29346  usgrexmpldifpr  29352  usgrexmpledg  29356  uhgrsubgrself  29374  uhgrspan1lem1  29394  upgrres1lem1  29403  fusgrfis  29424  vtxd0nedgb  29582  p1evtxdeqlem  29606  p1evtxdeq  29607  p1evtxdp1  29608  umgr2v2e  29619  vdegp1bi  29631  wlkcomp  29724  upgr2pthnlp  29825  usgr2trlncl  29853  usgr2pthlem  29856  clwlkcomp  29872  uspgrn2crct  29901  wwlksonvtx  29948  wspthnonp  29952  2wlkond  30030  2pthond  30035  2pthon3v  30036  umgr2adedgwlkonALT  30040  umgr2wlk  30042  umgr2wlkon  30043  wpthswwlks2on  30057  elwspths2spth  30063  0ewlk  30209  0pth  30220  0pthonv  30224  1pthon2v  30248  3wlkdlem4  30257  3trlond  30268  3pthond  30270  3spthond  30272  trlsegvdeglem3  30317  eupthvdres  30330  eupth2lemb  30332  ex-natded5.2i  30501  ex-an  30517  ex-id  30529  ex-po  30530  ex-fl  30542  ex-mod  30544  ex-exp  30545  ex-lcm  30553  nvz0  30764  ipidsq  30806  ipdirilem  30925  siilem1  30947  minvecolem2  30971  minvecolem3  30972  minvecolem4  30976  hvsubcan  31170  hvsubcan2  31171  normlem7tALT  31215  helch  31339  hsn0elch  31344  hhshsslem2  31364  hhsssh  31365  shscli  31413  shintcli  31425  shintcl  31426  chintcli  31427  chintcl  31428  shincli  31458  shsval2i  31483  omlsi  31500  chincli  31556  chabs1  31612  fh1i  31717  fh2i  31718  cm2ji  31721  pjnormi  31817  nmopsetn0  31961  nmfnsetn0  31974  lnophm  32115  nmcexi  32122  nmbdfnlb  32146  imaelshi  32154  nlelshi  32156  nmopadjlem  32185  nmopcoadji  32197  hmopidmch  32249  hmopidmpj  32250  sto1i  32332  stlei  32336  stji1i  32338  csmdsymi  32430  chirred  32491  cdj3lem1  32530  rpdp2cl  32967  dp2lt10  32969  dp2lt  32970  dp2ltc  32972  dpfrac1  32977  dplti  32990  dpgti  32991  dpexpp1  32993  dpadd3  32997  dpmul  32998  dpmul4  32999  xrsclat  33097  nn0archi  33437  zringfrac  33644  cos9thpiminplylem4  33976  cos9thpiminplylem5  33977  cos9thpinconstr  33982  lmatfvlem  34006  xrge0iifmhm  34130  qqh0  34175  qqh1  34176  rerrext  34200  cnrrext  34201  prsiga  34322  oms0  34488  coinfliprv  34674  ballotlem1  34678  ballotth  34729  signsw0g  34747  hgt750lemd  34839  hgt750lem  34842  hgt750lem2  34843  hgt750leme  34849  tgoldbachgt  34854  subfacval2  35422  erdszelem2  35427  cvmliftlem4  35523  satom  35591  satfv1  35598  sat1el2xp  35614  fmlaomn0  35625  satfdmfmla  35635  satfv1fvfmla1  35658  ex-sategoelelomsuc  35661  ex-sategoelel12  35662  prv0  35665  prv1n  35666  elmrsubrn  35755  msubfval  35759  problem4  35903  quad3  35905  br6  35992  dfon2lem3  36018  fullfunfnv  36181  itgeq12i  36441  fneref  36585  filnetlem2  36614  filnetlem3  36615  onpsstopbas  36665  dfttc3gw  36758  dfttc4lem2  36764  dnizeq0  36788  dnibndlem12  36802  knoppcnlem5  36810  knoppcnlem8  36813  knoppcnlem11  36816  knoppndvlem14  36838  cnndvlem1  36850  bj-genr  36925  bj-genl  36926  bj-genan  36927  bj-2upln1upl  37384  bj-vtoclgfALT  37419  bj-brab2a1  37516  bj-opabssvv  37517  taupilem1  37688  qdiff  37694  topdifinf  37718  sin2h  37984  cos2h  37985  tan2h  37986  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem11  38005  poimirlem12  38006  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem22  38016  poimirlem23  38017  poimirlem24  38018  poimirlem25  38019  poimirlem26  38020  poimirlem29  38023  poimirlem31  38025  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  itg2addnclem2  38046  asindmre  38077  heiborlem7  38191  riscer  38362  refrelcoss3  38927  symrelcoss3  38929  ishlatiN  39854  0psubN  40248  atpsubN  40252  gcdcomnni  42480  gcdnegnni  42481  neggcdnni  42482  60gcd7e1  42497  lcmeprodgcdi  42499  lcm2un  42506  lcm3un  42507  lcmineqlem4  42524  lcmineqlem6  42526  3lexlogpow5ineq1  42546  aks4d1p1p2  42562  mzpclall  43183  diophin  43228  diophun  43229  eldioph4b  43263  irrapx1  43280  2nn0ind  43397  aomclem4  43509  onexlimgt  43695  nnoeomeqom  43764  oaomoencom  43769  oenassex  43770  succlg  43780  dflim5  43781  omabs2  43784  tfsconcatfv2  43792  ifpid3g  43943  ifpid2g  43944  ifpbi1b  43954  eu0  43971  pwinfi  44015  rtrclex  44068  cnvrcl0  44076  dfrcl2  44125  relexp1idm  44165  relexp0idm  44166  clsk1independent  44497  lhe4.4ex1a  44780  expgrowth  44786  ax6e2nd  45009  uun0.1  45228  relopabVD  45351  ax6e2ndVD  45358  sb5ALTVD  45363  ax6e2ndALT  45380  permaxinf2lem  45463  rexanuz2nf  45942  dvmptconst  46365  dvmptidg  46367  dvmulcncf  46375  dvdivcncf  46377  dvnprodlem3  46398  itgsinexplem1  46404  volioof  46437  stoweidlem13  46463  stoweidlem14  46464  stoweidlem26  46476  stoweidlem34  46484  stoweidlem49  46499  stoweidlem59  46509  dirkertrigeqlem3  46550  dirkercncflem1  46553  dirkercncflem2  46554  fourierdlem57  46613  fourierdlem62  46618  fourierdlem103  46659  fourierdlem111  46667  fourierswlem  46680  fouriersw  46681  salexct2  46789  salexct3  46792  salgencntex  46793  salgensscntex  46794  gsumge0cl  46821  sge00  46826  sge0tsms  46830  0ome  46979  ovnlecvr  47008  ovn0lem  47015  hoidmvle  47050  ovnsubadd2lem  47095  smflimlem6  47226  mbfpsssmf  47233  smfmullem4  47244  smfpimbor1lem1  47248  nthrucw  47338  goldratmolem2  47356  cjnpoly  47359  sinnpoly  47361  astbstanbst  47379  aistbistaandb  47380  abnotataxb  47386  aifftbifffaibif  47391  confun4  47412  plcofph  47414  plvcofph  47416  plvcofphax  47417  plvofpos  47418  mdandyv0  47419  mdandyv1  47420  mdandyv2  47421  mdandyv3  47422  mdandyv4  47423  mdandyv5  47424  mdandyv6  47425  mdandyv7  47426  mdandyv8  47427  mdandyv9  47428  mdandyv10  47429  mdandyv11  47430  mdandyv12  47431  mdandyv13  47432  mdandyv14  47433  mdandyv15  47434  mdandyvr0  47435  mdandyvr1  47436  mdandyvr2  47437  mdandyvr3  47438  mdandyvr4  47439  mdandyvr5  47440  mdandyvr6  47441  mdandyvr7  47442  mdandyvrx0  47451  mdandyvrx1  47452  mdandyvrx2  47453  mdandyvrx3  47454  mdandyvrx4  47455  mdandyvrx5  47456  mdandyvrx6  47457  mdandyvrx7  47458  dandysum2p2e4  47468  or2expropbilem1  47502  dfnelbr2  47743  2ltceilhalf  47802  flmrecm1  47813  ich2exprop  47953  paireqne  47993  fmtno4prmfac  48057  31prm  48082  lighneallem4a  48093  41prothprmlem2  48103  ppivalnn4  48112  zofldiv2ALTV  48160  nfermltl8rev  48240  nfermltl2rev  48241  nfermltlrev  48242  gbegt5  48259  gbowgt5  48260  gboge9  48262  9gbo  48272  11gbo  48273  nnsum3primes4  48286  nnsum3primesgbe  48290  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  tgblthelfgott  48313  tgoldbach  48315  ushggricedg  48425  isubgrgrim  48427  stgrvtx  48452  stgriedg  48453  stgrusgra  48457  stgr1  48459  uspgrlim  48490  grlimprclnbgrvtx  48497  clnbgr3stgrgrlic  48518  usgrexmpl1lem  48519  usgrexmpl2lem  48524  usgrexmpl2nb0  48529  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  usgrexmpl2nb3  48532  usgrexmpl2nb4  48533  usgrexmpl2nb5  48534  gpgvtx  48541  gpgiedg  48542  gpgorder  48557  gpgvtxedg0  48561  gpgvtxedg1  48562  gpgedgiov  48563  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem2  48570  gpg5nbgrvtx13starlem3  48571  gpg3kgrtriexlem3  48583  gpg3kgrtriexlem6  48586  gpgprismgr4cycllem2  48594  gpgprismgr4cyclex  48605  pgnioedg1  48606  pgnioedg2  48607  pgnioedg3  48608  pgnioedg4  48609  pgnioedg5  48610  pgnbgreunbgrlem2lem1  48612  pgnbgreunbgrlem2lem2  48613  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem4  48617  pgnbgreunbgrlem5lem1  48618  pgnbgreunbgrlem5lem2  48619  pgnbgreunbgrlem5lem3  48620  pgnbgreunbgrlem6  48622  gpg5ngric  48626  gpg5edgnedg  48628  nn0mnd  48677  mgmplusgiopALT  48692  sgrp2sgrp  48726  2zrngaabl  48748  funcringcsetcALTV2lem8  48795  funcringcsetclem8ALTV  48818  zlmodzxzlmod  48852  zlmodzxzel  48853  zlmodzxzscm  48855  zlmodzxzadd  48856  snlindsntorlem  48968  ldepspr  48971  lmod1lem2  48986  lmod1lem3  48987  lmod1lem4  48988  lmod1lem5  48989  lmodn0  48993  zlmodzxznm  48995  zlmodzxzldeplem  48996  zlmodzxzldeplem1  48998  zlmodzxzldeplem3  49000  lvecpsslmod  49005  ldepsnlinc  49006  ldepslinc  49007  expnegico01  49016  zofldiv2  49029  flnn0div2ge  49031  elbigo2  49050  nnlog2ge0lt1  49064  digfval  49095  dignnld  49101  dignn0flhalf  49116  2arymaptfo  49152  itcovalt2lem1  49173  prelrrx2  49211  eenglngeehlnmlem2  49236  rrxsphere  49246  line2  49250  line2x  49252  line2y  49253  itsclc0yqsollem2  49261  inlinecirc02plem  49284  sepfsepc  49425  invfn  49527  alimp-surprise  50277  aacllem  50298