Theorem pm3.2i 476

Description: Infer conjunction of premises. Inference associated with pm3.2 475. Its associated deduction is jca 521 (and the double deduction is jcad 522). (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 475	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
4	1, 2, 3	mp2 9	1 ⊢ (𝜑 ∧ 𝜓)

This proof depends on syntax axioms:   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mp4an  706  pm4.87  857  3pm3.2i  1358  unssi  4137  ssini  4185  opthhausdorff  5490  elvv  5726  elopaelxp  5741  relopabiv  5798  relopabi  5800  dfpo2  6299  funpr  6596  funcnvpr  6602  mpov  7532  caovcom  7618  snnex  7772  pwnex  7773  1st2val  8029  2nd2val  8030  elxp7  8036  opreuopreu  8046  poxp2  8160  poseq  8175  tfr1a  8402  oeoa  8606  oeoe  8608  erov  8835  endisj  9083  snopfsupp  9383  ssttrcl  9716  ttrclselem2  9727  r1funlimOLD  9770  dfac2b  10209  cflecard  10330  canth4  10732  canthnumlem  10733  canthwelem  10735  canthp1lem2  10738  pwfseqlem4  10747  wunex3  10826  addsrpr  11160  mulsrpr  11161  recexsrlem  11188  mulcani  11955  div1  12006  recdiv  12023  divdiv1  12028  divdiv2  12029  div23i  12075  div11i  12076  divmuldivi  12077  divadddivi  12079  divdivdivi  12080  lemulge11  12179  negiso  12297  dfnn3  12349  2cnne0  12555  2rene0  12556  halfpm6th  12568  avglt1  12584  avglt2  12585  div4p1lem1div2  12601  3halfnz  12778  divlt1lt  13191  divle1le  13192  nnledivrp  13234  x2times  13429  xrsupsslem  13437  xrinfmsslem  13438  nnge2recico01  13638  fvf1tp  13929  om2uzoi  14098  fzennn  14111  expge1  14242  sqoddm1div8  14387  faclbnd2  14435  faclbnd4lem1  14437  4bc2eq6  14473  hashfxnn0  14481  hashsnlei  14563  hashunlei  14570  hashsslei  14571  hash2prb  14617  repswccat  14937  funcnvs4  15066  f1oun2prg  15068  wrdlen2i  15093  s2rn  15116  s3rn  15117  s7rn  15118  relexpaddg  15206  cjreb  15290  sqrt2gt1lt2  15441  abs1m  15503  bpoly3  16224  ege2le3  16256  efi4p  16305  efival  16320  sin01bnd  16353  cos01bnd  16354  cos1bnd  16355  cos2bnd  16356  sin01gt0  16358  cos01gt0  16359  sin02gt0  16360  sincos2sgn  16362  sin4lt0  16363  egt2lt3  16374  rpnnen2lem3  16384  rpnnen2lem11  16392  nthruc  16420  nthruz  16421  3dvdsdec  16502  3dvds2dec  16503  mod2eq1n2dvds  16517  halfleoddlt  16532  divalglem5  16567  ndvdsi  16582  flodddiv4  16585  flodddiv4lt  16587  bitsp1o  16603  3lcm2e6woprm  16790  6lcm4e12  16791  pcrec  17036  prmrec  17100  prmgaplcmlem1  17229  prmgaplcm  17238  modsubi  17250  structfn  17334  strleun  17335  slotsdifipndx  17506  slotsdifplendx  17546  slotsdifdsndx  17565  slotsdifunifndx  17572  slotsdifplendx2  17587  slotsdifocndx  17588  isofn  17950  sscres  17998  funcestrcsetclem7  18320  funcestrcsetclem8  18321  fullestrcsetc  18325  nulchn  18793  chninf  18809  mgmnsgrpex  19130  degenmgm  19137  degenmgm2nfun  19139  degenmgm2  19140  pwmnd  19143  ga0  19512  symg2bas  19607  f1otrspeq  19661  psgnsn  19734  0frgp  19993  gsummptnn0fz  20200  srgbinomlem4  20455  isrnghm  20671  rnghmsscmap2  20881  rnghmsscmap  20882  funcrngcsetc  20892  funcrngcsetcALT  20893  rhmsscmap2  20910  rhmsscmap  20911  funcringcsetc  20926  cnfldfun  21692  cnfldfunALT  21693  cnfld1  21703  cnsubdrglem  21724  expmhm  21742  expghm  21781  pzriprnglem4  21790  pzriprnglem9  21795  pzriprnglem14  21800  pzriprng1ALT  21802  psrbag0  22371  psrbagsn  22372  coe1fsupp  22532  coe1mul2  22588  evls1sca  22641  matmulr  22753  mat1dimelbas  22786  mat1f1o  22793  m2detleib  22946  smadiadetglem1  22986  pmatcollpw3fi1lem2  23105  cpmidpmatlem2  23189  cpmadumatpolylem1  23199  cayhamlem3  23205  cayhamlem4  23206  isbasis3g  23267  fctop  23322  cctop  23324  refref  23832  bl2in  24719  dscmet  24891  iihalf1  25252  iihalf2  25254  icopnfhmeo  25264  iccpnfhmeo  25266  xrhmeo  25267  iscvsi  25450  zclmncvs  25469  ncvs1  25478  ehl2eudis  25743  minveclem2  25747  minveclem4  25753  ovolunlem1a  25817  volf  25850  i1f1lem  26010  mbfi1fseqlem5  26040  dveflem  26299  pilem2  26779  pilem3  26780  sinhalfpilem  26792  sincosq1lem  26826  tangtx  26834  sinq12gt0  26836  sincos4thpi  26842  sincos6thpi  26844  sincos3rdpi  26845  pigt3  26846  pige3ALT  26848  coseq1  26853  efeq1  26856  efif1olem4  26873  angneg  27131  ang180lem1  27137  1cubrlem  27169  quart1  27184  log2cnv  27272  log2tlbnd  27273  log2ublem1  27274  log2ub  27277  emcllem1  27323  emcllem6  27328  basellem1  27408  basellem2  27409  basellem3  27410  basellem8  27415  ppiublem1  27529  ppiublem2  27530  ppiub  27531  chtublem  27538  chtub  27539  bcmono  27604  bclbnd  27607  bpos1lem  27609  bposlem1  27611  bposlem2  27612  bposlem3  27613  bposlem4  27614  bposlem5  27615  bposlem6  27616  bposlem7  27617  bposlem8  27618  bposlem9  27619  lgsdir2lem1  27652  1lgs  27667  gausslemma2dlem0c  27685  gausslemma2dlem0d  27686  gausslemma2dlem1a  27692  gausslemma2dlem2  27694  gausslemma2dlem3  27695  gausslemma2dlem5  27698  gausslemma2dlem6  27699  lgsquad2lem2  27712  2lgslem1a1  27716  2lgslem1a2  27717  2lgslem1c  27720  2lgslem3a  27723  2lgslem3b  27724  2lgslem3c  27725  2lgslem3d  27726  2lgslem3  27731  2lgsoddprmlem1  27735  addsqrexnreu  27769  addsqnreup  27770  chebbnd1lem1  27796  chebbnd1lem3  27798  chebbnd1  27799  dchrisum0flblem2  27836  dchrisum0lem1  27843  mulog2sumlem2  27862  selberglem2  27873  chpdifbndlem1  27880  sltssnb  28155  mulscl  28520  ltmuls  28522  divs1  28590  precsexlem8  28600  0reno  28882  1reno  28883  slotsinbpsd  28903  slotslnbpsd  28904  ercgrg  28980  axlowdimlem4  29523  axlowdimlem5  29524  axlowdimlem6  29525  axlowdimlem7  29526  axlowdimlem8  29527  axlowdimlem10  29529  axlowdimlem11  29530  graop  29607  grastruct  29608  uhgrunop  29653  upgrop  29672  upgrunop  29697  umgrunop  29699  usgrop  29744  usgr2v1e2w  29833  usgrexmpldifpr  29839  usgrexmpledg  29843  uhgrsubgrself  29861  uhgrspan1lem1  29881  upgrres1lem1  29890  fusgrfis  29911  vtxd0nedgb  30069  p1evtxdeqlem  30093  p1evtxdeq  30094  p1evtxdp1  30095  umgr2v2e  30106  vdegp1bi  30118  wlkcomp  30211  upgr2pthnlp  30318  usgr2trlncl  30346  usgr2pthlem  30349  clwlkcomp  30366  uspgrn2crct  30397  wwlksonvtx  30444  wspthnonp  30448  2wlkond  30526  2pthond  30531  2pthon3v  30532  umgr2adedgwlkonALT  30536  umgr2wlk  30538  umgr2wlkon  30539  wpthswwlks2on  30553  elwspths2spth  30559  0ewlk  30705  0pth  30716  0pthonv  30720  1pthon2v  30754  3wlkdlem4  30763  3trlond  30774  3pthond  30776  3spthond  30778  trlsegvdeglem3  30823  eupthvdres  30836  eupth2lemb  30838  ex-natded5.2i  31007  ex-an  31023  ex-id  31035  ex-po  31036  ex-fl  31048  ex-mod  31050  ex-exp  31051  ex-lcm  31059  nvz0  31270  ipidsq  31312  ipdirilem  31431  siilem1  31453  minvecolem2  31477  minvecolem3  31478  minvecolem4  31482  hvsubcan  31676  hvsubcan2  31677  normlem7tALT  31721  helch  31845  hsn0elch  31850  hhshsslem2  31870  hhsssh  31871  shscli  31919  shintcli  31931  shintcl  31932  chintcli  31933  chintcl  31934  shincli  31964  shsval2i  31989  omlsi  32006  chincli  32062  chabs1  32118  fh1i  32223  fh2i  32224  cm2ji  32227  pjnormi  32323  nmopsetn0  32467  nmfnsetn0  32480  lnophm  32621  nmcexi  32628  nmbdfnlb  32652  imaelshi  32660  nlelshi  32662  nmopadjlem  32691  nmopcoadji  32703  hmopidmch  32755  hmopidmpj  32756  sto1i  32838  stlei  32842  stji1i  32844  csmdsymi  32936  chirred  32997  cdj3lem1  33036  rpdp2cl  33448  dp2lt10  33450  dp2lt  33451  dp2ltc  33453  dpfrac1  33458  dplti  33471  dpgti  33472  dpexpp1  33474  dpadd3  33478  dpmul  33479  dpmul4  33480  xrsclat  33572  nn0archi  33908  zringfrac  34086  cos9thpiminplylem4  34417  cos9thpiminplylem5  34418  cos9thpinconstr  34423  lmatfvlem  34447  xrge0iifmhm  34571  qqh0  34616  qqh1  34617  rerrext  34641  cnrrext  34642  prsiga  34763  oms0  34929  coinfliprv  35115  ballotlem1  35119  ballotth  35170  signsw0g  35185  hgt750lemd  35277  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  tgoldbachgt  35292  subfacval2  35952  erdszelem2  35957  cvmliftlem4  36053  satom  36121  satfv1  36128  sat1el2xp  36144  fmlaomn0  36155  satfdmfmla  36165  satfv1fvfmla1  36188  ex-sategoelelomsuc  36191  ex-sategoelel12  36192  prv0  36195  prv1n  36196  elmrsubrn  36285  msubfval  36289  problem4  36433  quad3  36435  br6  36522  dfon2lem3  36547  fullfunfnv  36710  itgeq12i  36995  fneref  37138  filnetlem2  37167  filnetlem3  37168  onpsstopbas  37218  dfttc3gw  37311  dfttc4lem2  37317  dnizeq0  37341  dnibndlem12  37355  knoppcnlem5  37363  knoppcnlem8  37366  knoppcnlem11  37369  knoppndvlem14  37391  cnndvlem1  37403  bj-genr  37477  bj-genl  37478  bj-genan  37479  bj-2upln1upl  37937  coi1in  37961  bj-vtoclgfALT  37974  bj-brab2a1  38071  bj-opabssvv  38072  taupilem1  38243  qdiff  38249  topdifinf  38273  sin2h  38534  cos2h  38535  tan2h  38536  poimirlem1  38540  poimirlem2  38541  poimirlem3  38542  poimirlem4  38543  poimirlem6  38545  poimirlem7  38546  poimirlem11  38550  poimirlem12  38551  poimirlem16  38555  poimirlem17  38556  poimirlem19  38558  poimirlem20  38559  poimirlem22  38561  poimirlem23  38562  poimirlem24  38563  poimirlem25  38564  poimirlem26  38565  poimirlem29  38568  poimirlem31  38570  mblfinlem3  38578  mblfinlem4  38579  ismblfin  38580  itg2addnclem2  38591  asindmre  38622  heiborlem7  38752  riscer  38923  refrelcoss3  39486  symrelcoss3  39488  ishlatiN  40413  0psubN  40807  atpsubN  40811  gcdcomnni  43039  gcdnegnni  43040  neggcdnni  43041  60gcd7e1  43056  lcmeprodgcdi  43058  lcm2un  43065  lcm3un  43066  lcmineqlem4  43083  lcmineqlem6  43085  3lexlogpow5ineq1  43105  aks4d1p1p2  43121  25or6to4  43257  mzpclall  43738  diophin  43783  diophun  43784  eldioph4b  43818  irrapx1  43835  2nn0ind  43952  aomclem4  44059  onexlimgt  44245  nnoeomeqom  44314  oaomoencom  44319  oenassex  44320  succlg  44330  dflim5  44331  omabs2  44334  tfsconcatfv2  44342  ifpid3g  44493  ifpid2g  44494  ifpbi1b  44504  eu0  44521  pwinfi  44565  rtrclex  44617  cnvrcl0  44625  dfrcl2  44674  relexp1idm  44714  relexp0idm  44715  clsk1independent  45046  lhe4.4ex1a  45313  expgrowth  45319  ax6e2nd  45541  uun0.1  45760  relopabVD  45883  ax6e2ndVD  45890  sb5ALTVD  45895  ax6e2ndALT  45912  permaxinf2lem  46002  rexanuz2nf  46502  dvmptconst  46925  dvmptidg  46927  dvmulcncf  46935  dvdivcncf  46937  dvnprodlem3  46958  itgsinexplem1  46964  volioof  46997  stoweidlem13  47023  stoweidlem14  47024  stoweidlem26  47036  stoweidlem34  47044  stoweidlem49  47059  stoweidlem59  47069  dirkertrigeqlem3  47110  dirkercncflem1  47113  dirkercncflem2  47114  fourierdlem57  47173  fourierdlem62  47178  fourierdlem103  47219  fourierdlem111  47227  fourierswlem  47240  fouriersw  47241  salexct2  47349  salexct3  47352  salgencntex  47353  salgensscntex  47354  gsumge0cl  47381  sge00  47386  sge0tsms  47390  0ome  47539  ovnlecvr  47568  ovn0lem  47575  hoidmvle  47610  ovnsubadd2lem  47655  smflimlem6  47786  mbfpsssmf  47793  smfmullem4  47804  smfpimbor1lem1  47808  sqrtnzqaa  47914  numtowerdt  47916  goldratmolem2  47933  sqrtnpoly  47943  astbstanbst  47979  aistbistaandb  47980  abnotataxb  47986  aifftbifffaibif  47991  confun4  48012  plcofph  48014  plvcofph  48016  plvcofphax  48017  plvofpos  48018  mdandyv0  48019  mdandyv1  48020  mdandyv2  48021  mdandyv3  48022  mdandyv4  48023  mdandyv5  48024  mdandyv6  48025  mdandyv7  48026  mdandyv8  48027  mdandyv9  48028  mdandyv10  48029  mdandyv11  48030  mdandyv12  48031  mdandyv13  48032  mdandyv14  48033  mdandyv15  48034  mdandyvr0  48035  mdandyvr1  48036  mdandyvr2  48037  mdandyvr3  48038  mdandyvr4  48039  mdandyvr5  48040  mdandyvr6  48041  mdandyvr7  48042  mdandyvrx0  48051  mdandyvrx1  48052  mdandyvrx2  48053  mdandyvrx3  48054  mdandyvrx4  48055  mdandyvrx5  48056  mdandyvrx6  48057  mdandyvrx7  48058  dandysum2p2e4  48068  or2expropbilem1  48102  dfnelbr2  48343  2ltceilhalf  48402  flmrecm1  48413  ich2exprop  48553  paireqne  48593  fmtno4prmfac  48657  31prm  48682  lighneallem4a  48693  41prothprmlem2  48703  ppivalnn4  48712  zofldiv2ALTV  48760  nfermltl8rev  48840  nfermltl2rev  48841  nfermltlrev  48842  gbegt5  48859  gbowgt5  48860  gboge9  48862  9gbo  48872  11gbo  48873  nnsum3primes4  48886  nnsum3primesgbe  48890  nnsum4primesodd  48894  nnsum4primesoddALTV  48895  nnsum4primeseven  48898  nnsum4primesevenALTV  48899  tgblthelfgott  48913  tgoldbach  48915  ushggricedg  49025  isubgrgrim  49027  stgrvtx  49052  stgriedg  49053  stgrusgra  49057  stgr1  49059  uspgrlim  49090  grlimprclnbgrvtx  49097  clnbgr3stgrgrlic  49118  usgrexmpl1lem  49119  usgrexmpl2lem  49124  usgrexmpl2nb0  49129  usgrexmpl2nb1  49130  usgrexmpl2nb2  49131  usgrexmpl2nb3  49132  usgrexmpl2nb4  49133  usgrexmpl2nb5  49134  gpgvtx  49141  gpgiedg  49142  gpgorder  49157  gpgvtxedg0  49161  gpgvtxedg1  49162  gpgedgiov  49163  gpg5nbgrvtx03starlem1  49166  gpg5nbgrvtx03starlem2  49167  gpg5nbgrvtx03starlem3  49168  gpg5nbgrvtx13starlem1  49169  gpg5nbgrvtx13starlem2  49170  gpg5nbgrvtx13starlem3  49171  gpg3kgrtriexlem3  49183  gpg3kgrtriexlem6  49186  gpgprismgr4cycllem2  49194  gpgprismgr4cyclex  49205  pgnioedg1  49206  pgnioedg2  49207  pgnioedg3  49208  pgnioedg4  49209  pgnioedg5  49210  pgnbgreunbgrlem2lem1  49212  pgnbgreunbgrlem2lem2  49213  pgnbgreunbgrlem2lem3  49214  pgnbgreunbgrlem3  49216  pgnbgreunbgrlem4  49217  pgnbgreunbgrlem5lem1  49218  pgnbgreunbgrlem5lem2  49219  pgnbgreunbgrlem5lem3  49220  pgnbgreunbgrlem6  49222  gpg5ngric  49226  gpg5edgnedg  49228  nn0mnd  49276  mgmplusgiopALT  49291  sgrp2sgrp  49325  2zrngaabl  49347  funcringcsetcALTV2lem8  49394  funcringcsetclem8ALTV  49417  zlmodzxzlmod  49466  zlmodzxzel  49467  zlmodzxzscm  49469  zlmodzxzadd  49470  snlindsntorlem  49582  ldepspr  49585  lmod1lem2  49600  lmod1lem3  49601  lmod1lem4  49602  lmod1lem5  49603  lmodn0  49607  zlmodzxznm  49609  zlmodzxzldeplem  49610  zlmodzxzldeplem1  49612  zlmodzxzldeplem3  49614  lvecpsslmod  49619  ldepsnlinc  49620  ldepslinc  49621  expnegico01  49630  zofldiv2  49643  flnn0div2ge  49645  elbigo2  49664  nnlog2ge0lt1  49678  digfval  49709  dignnld  49715  dignn0flhalf  49730  2arymaptfo  49766  itcovalt2lem1  49787  prelrrx2  49825  eenglngeehlnmlem2  49850  rrxsphere  49860  line2  49864  line2x  49866  line2y  49867  itsclc0yqsollem2  49875  inlinecirc02plem  49898  sepfsepc  50036  invfn  50138  alimp-surprise  50876  aacllem  50939