Theorem pm3.2i 470

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

Syntax hints:   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mp4an  693  pm4.87  843  3pm3.2i  1340  unssi  4143  ssini  4192  opthhausdorff  5465  elvv  5699  elopaelxp  5714  relopabiv  5769  relopabi  5771  dfpo2  6254  funpr  6548  funcnvpr  6554  mpov  7470  caovcom  7555  snnex  7703  pwnex  7704  1st2val  7961  2nd2val  7962  elxp7  7968  opreuopreu  7978  poxp2  8085  poseq  8100  tfr1a  8325  oeoa  8525  oeoe  8527  erov  8751  endisj  8992  snopfsupp  9294  ssttrcl  9624  ttrclselem2  9635  r1funlim  9678  dfac2b  10041  cflecard  10163  canth4  10558  canthnumlem  10559  canthwelem  10561  canthp1lem2  10564  pwfseqlem4  10573  wunex3  10652  addsrpr  10986  mulsrpr  10987  recexsrlem  11014  mulcani  11776  div1  11831  recdiv  11847  divdiv1  11852  divdiv2  11853  div23i  11899  div11i  11900  divmuldivi  11901  divadddivi  11903  divdivdivi  11904  lemulge11  12004  negiso  12122  dfnn3  12159  2cnne0  12350  2rene0  12351  halfpm6th  12363  avglt1  12379  avglt2  12380  div4p1lem1div2  12396  3halfnz  12571  divlt1lt  12976  divle1le  12977  nnledivrp  13019  x2times  13214  xrsupsslem  13222  xrinfmsslem  13223  fvf1tp  13709  om2uzoi  13878  fzennn  13891  expge1  14022  sqoddm1div8  14166  faclbnd2  14214  faclbnd4lem1  14216  4bc2eq6  14252  hashfxnn0  14260  hashsnlei  14341  hashunlei  14348  hashsslei  14349  hash2prb  14395  repswccat  14709  funcnvs4  14838  f1oun2prg  14840  wrdlen2i  14865  s2rn  14886  s3rn  14887  s7rn  14888  relexpaddg  14976  cjreb  15046  sqrt2gt1lt2  15197  abs1m  15259  bpoly3  15981  ege2le3  16013  efi4p  16062  efival  16077  sin01bnd  16110  cos01bnd  16111  cos1bnd  16112  cos2bnd  16113  sin01gt0  16115  cos01gt0  16116  sin02gt0  16117  sincos2sgn  16119  sin4lt0  16120  egt2lt3  16131  rpnnen2lem3  16141  rpnnen2lem11  16149  nthruc  16177  nthruz  16178  3dvdsdec  16259  3dvds2dec  16260  mod2eq1n2dvds  16274  halfleoddlt  16289  divalglem5  16324  ndvdsi  16339  flodddiv4  16342  flodddiv4lt  16344  bitsp1o  16360  3lcm2e6woprm  16542  6lcm4e12  16543  pcrec  16786  prmrec  16850  prmgaplcmlem1  16979  prmgaplcm  16988  modsubi  17000  structfn  17083  strleun  17084  slotsdifipndx  17255  slotsdifplendx  17295  slotsdifdsndx  17314  slotsdifunifndx  17321  slotsdifplendx2  17336  slotsdifocndx  17337  isofn  17699  sscres  17747  funcestrcsetclem7  18069  funcestrcsetclem8  18070  fullestrcsetc  18074  nulchn  18542  chninf  18558  mgmnsgrpex  18856  pwmnd  18862  ga0  19227  symg2bas  19322  f1otrspeq  19376  psgnsn  19449  0frgp  19708  gsummptnn0fz  19915  srgbinomlem4  20164  isrnghm  20377  rnghmsscmap2  20562  rnghmsscmap  20563  funcrngcsetc  20573  funcrngcsetcALT  20574  rhmsscmap2  20591  rhmsscmap  20592  funcringcsetc  20607  cnfldfun  21323  cnfldfunALT  21324  cnfldfunOLD  21336  cnfldfunALTOLD  21337  cnfld1  21348  cnfld1OLD  21349  cnsubdrglem  21373  expmhm  21391  expghm  21430  pzriprnglem4  21439  pzriprnglem9  21444  pzriprnglem14  21449  pzriprng1ALT  21451  psrbag0  22017  psrbagsn  22018  coe1fsupp  22155  coe1mul2  22211  evls1sca  22267  matmulr  22382  mat1dimelbas  22415  mat1f1o  22422  m2detleib  22575  smadiadetglem1  22615  pmatcollpw3fi1lem2  22731  cpmidpmatlem2  22815  cpmadumatpolylem1  22825  cayhamlem3  22831  cayhamlem4  22832  isbasis3g  22893  fctop  22948  cctop  22950  refref  23457  bl2in  24344  dscmet  24516  iihalf1  24881  iihalf2  24884  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  iscvsi  25085  zclmncvs  25104  ncvs1  25113  ehl2eudis  25378  minveclem2  25382  minveclem4  25388  ovolunlem1a  25453  volf  25486  i1f1lem  25646  mbfi1fseqlem5  25676  dveflem  25939  pilem2  26418  pilem3  26419  sinhalfpilem  26428  sincosq1lem  26462  tangtx  26470  sinq12gt0  26472  sincos4thpi  26478  sincos6thpi  26481  sincos3rdpi  26482  pigt3  26483  pige3ALT  26485  coseq1  26490  efeq1  26493  efif1olem4  26510  angneg  26769  ang180lem1  26775  1cubrlem  26807  quart1  26822  log2cnv  26910  log2tlbnd  26911  log2ublem1  26912  log2ub  26915  emcllem1  26962  emcllem6  26967  basellem1  27047  basellem2  27048  basellem3  27049  basellem8  27054  ppiublem1  27169  ppiublem2  27170  ppiub  27171  chtublem  27178  chtub  27179  bcmono  27244  bclbnd  27247  bpos1lem  27249  bposlem1  27251  bposlem2  27252  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem6  27256  bposlem7  27257  bposlem8  27258  bposlem9  27259  lgsdir2lem1  27292  1lgs  27307  gausslemma2dlem0c  27325  gausslemma2dlem0d  27326  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  gausslemma2dlem3  27335  gausslemma2dlem5  27338  gausslemma2dlem6  27339  lgsquad2lem2  27352  2lgslem1a1  27356  2lgslem1a2  27357  2lgslem1c  27360  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2lgslem3  27371  2lgsoddprmlem1  27375  addsqrexnreu  27409  addsqnreup  27410  chebbnd1lem1  27436  chebbnd1lem3  27438  chebbnd1  27439  dchrisum0flblem2  27476  dchrisum0lem1  27483  mulog2sumlem2  27502  selberglem2  27513  chpdifbndlem1  27520  sltssnb  27765  mulscl  28130  ltmuls  28132  divs1  28200  precsexlem8  28210  0reno  28492  1reno  28493  slotsinbpsd  28513  slotslnbpsd  28514  ercgrg  28589  axlowdimlem4  29018  axlowdimlem5  29019  axlowdimlem6  29020  axlowdimlem7  29021  axlowdimlem8  29022  axlowdimlem10  29024  axlowdimlem11  29025  graop  29102  grastruct  29103  uhgrunop  29148  upgrop  29167  upgrunop  29192  umgrunop  29194  usgrop  29236  usgr2v1e2w  29325  usgrexmpldifpr  29331  usgrexmpledg  29335  uhgrsubgrself  29353  uhgrspan1lem1  29373  upgrres1lem1  29382  fusgrfis  29403  vtxd0nedgb  29562  p1evtxdeqlem  29586  p1evtxdeq  29587  p1evtxdp1  29588  umgr2v2e  29599  vdegp1bi  29611  wlkcomp  29704  upgr2pthnlp  29805  usgr2trlncl  29833  usgr2pthlem  29836  clwlkcomp  29852  uspgrn2crct  29881  wwlksonvtx  29928  wspthnonp  29932  2wlkond  30010  2pthond  30015  2pthon3v  30016  umgr2adedgwlkonALT  30020  umgr2wlk  30022  umgr2wlkon  30023  wpthswwlks2on  30037  elwspths2spth  30043  0ewlk  30189  0pth  30200  0pthonv  30204  1pthon2v  30228  3wlkdlem4  30237  3trlond  30248  3pthond  30250  3spthond  30252  trlsegvdeglem3  30297  eupthvdres  30310  eupth2lemb  30312  ex-natded5.2i  30481  ex-an  30497  ex-id  30509  ex-po  30510  ex-fl  30522  ex-mod  30524  ex-exp  30525  ex-lcm  30533  nvz0  30743  ipidsq  30785  ipdirilem  30904  siilem1  30926  minvecolem2  30950  minvecolem3  30951  minvecolem4  30955  hvsubcan  31149  hvsubcan2  31150  normlem7tALT  31194  helch  31318  hsn0elch  31323  hhshsslem2  31343  hhsssh  31344  shscli  31392  shintcli  31404  shintcl  31405  chintcli  31406  chintcl  31407  shincli  31437  shsval2i  31462  omlsi  31479  chincli  31535  chabs1  31591  fh1i  31696  fh2i  31697  cm2ji  31700  pjnormi  31796  nmopsetn0  31940  nmfnsetn0  31953  lnophm  32094  nmcexi  32101  nmbdfnlb  32125  imaelshi  32133  nlelshi  32135  nmopadjlem  32164  nmopcoadji  32176  hmopidmch  32228  hmopidmpj  32229  sto1i  32311  stlei  32315  stji1i  32317  csmdsymi  32409  chirred  32470  cdj3lem1  32509  rpdp2cl  32963  dp2lt10  32965  dp2lt  32966  dp2ltc  32968  dpfrac1  32973  dplti  32986  dpgti  32987  dpexpp1  32989  dpadd3  32993  dpmul  32994  dpmul4  32995  xrsclat  33093  nn0archi  33428  zringfrac  33635  cos9thpiminplylem4  33942  cos9thpiminplylem5  33943  cos9thpinconstr  33948  lmatfvlem  33972  xrge0iifmhm  34096  qqh0  34141  qqh1  34142  rerrext  34166  cnrrext  34167  prsiga  34288  oms0  34454  coinfliprv  34640  ballotlem1  34644  ballotth  34695  signsw0g  34713  hgt750lemd  34805  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  tgoldbachgt  34820  subfacval2  35381  erdszelem2  35386  cvmliftlem4  35482  satom  35550  satfv1  35557  sat1el2xp  35573  fmlaomn0  35584  satfdmfmla  35594  satfv1fvfmla1  35617  ex-sategoelelomsuc  35620  ex-sategoelel12  35621  prv0  35624  prv1n  35625  elmrsubrn  35714  msubfval  35718  problem4  35862  quad3  35864  br6  35951  dfon2lem3  35977  fullfunfnv  36140  itgeq12i  36400  fneref  36544  filnetlem2  36573  filnetlem3  36574  onpsstopbas  36624  exeltr  36665  dnizeq0  36675  dnibndlem12  36689  knoppcnlem5  36697  knoppcnlem8  36700  knoppcnlem11  36703  knoppndvlem14  36725  cnndvlem1  36737  bj-genr  36806  bj-genl  36807  bj-genan  36808  bj-2upln1upl  37225  bj-vtoclgfALT  37260  bj-brab2a1  37350  bj-opabssvv  37351  taupilem1  37522  topdifinf  37550  sin2h  37807  cos2h  37808  tan2h  37809  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem4  37821  poimirlem6  37823  poimirlem7  37824  poimirlem11  37828  poimirlem12  37829  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem22  37839  poimirlem23  37840  poimirlem24  37841  poimirlem25  37842  poimirlem26  37843  poimirlem29  37846  poimirlem31  37848  mblfinlem3  37856  mblfinlem4  37857  ismblfin  37858  itg2addnclem2  37869  asindmre  37900  heiborlem7  38014  riscer  38185  refrelcoss3  38722  symrelcoss3  38724  ishlatiN  39611  0psubN  40005  atpsubN  40009  gcdcomnni  42238  gcdnegnni  42239  neggcdnni  42240  60gcd7e1  42255  lcmeprodgcdi  42257  lcm2un  42264  lcm3un  42265  lcmineqlem4  42282  lcmineqlem6  42284  3lexlogpow5ineq1  42304  aks4d1p1p2  42320  mzpclall  42965  diophin  43010  diophun  43011  eldioph4b  43049  irrapx1  43066  2nn0ind  43183  aomclem4  43295  onexlimgt  43481  nnoeomeqom  43550  oaomoencom  43555  oenassex  43556  succlg  43566  dflim5  43567  omabs2  43570  tfsconcatfv2  43578  ifpid3g  43729  ifpid2g  43730  ifpbi1b  43740  eu0  43757  pwinfi  43801  rtrclex  43854  cnvrcl0  43862  dfrcl2  43911  relexp1idm  43951  relexp0idm  43952  clsk1independent  44283  lhe4.4ex1a  44566  expgrowth  44572  ax6e2nd  44795  uun0.1  45014  relopabVD  45137  ax6e2ndVD  45144  sb5ALTVD  45149  ax6e2ndALT  45166  permaxinf2lem  45249  rexanuz2nf  45732  dvmptconst  46155  dvmptidg  46157  dvmulcncf  46165  dvdivcncf  46167  dvnprodlem3  46188  itgsinexplem1  46194  volioof  46227  stoweidlem13  46253  stoweidlem14  46254  stoweidlem26  46266  stoweidlem34  46274  stoweidlem49  46289  stoweidlem59  46299  dirkertrigeqlem3  46340  dirkercncflem1  46343  dirkercncflem2  46344  fourierdlem57  46403  fourierdlem62  46408  fourierdlem103  46449  fourierdlem111  46457  fourierswlem  46470  fouriersw  46471  salexct2  46579  salexct3  46582  salgencntex  46583  salgensscntex  46584  gsumge0cl  46611  sge00  46616  sge0tsms  46620  0ome  46769  ovnlecvr  46798  ovn0lem  46805  hoidmvle  46840  ovnsubadd2lem  46885  smflimlem6  47016  mbfpsssmf  47023  smfmullem4  47034  smfpimbor1lem1  47038  nthrucw  47126  cjnpoly  47131  sinnpoly  47133  astbstanbst  47151  aistbistaandb  47152  abnotataxb  47158  aifftbifffaibif  47163  confun4  47184  plcofph  47186  plvcofph  47188  plvcofphax  47189  plvofpos  47190  mdandyv0  47191  mdandyv1  47192  mdandyv2  47193  mdandyv3  47194  mdandyv4  47195  mdandyv5  47196  mdandyv6  47197  mdandyv7  47198  mdandyv8  47199  mdandyv9  47200  mdandyv10  47201  mdandyv11  47202  mdandyv12  47203  mdandyv13  47204  mdandyv14  47205  mdandyv15  47206  mdandyvr0  47207  mdandyvr1  47208  mdandyvr2  47209  mdandyvr3  47210  mdandyvr4  47211  mdandyvr5  47212  mdandyvr6  47213  mdandyvr7  47214  mdandyvrx0  47223  mdandyvrx1  47224  mdandyvrx2  47225  mdandyvrx3  47226  mdandyvrx4  47227  mdandyvrx5  47228  mdandyvrx6  47229  mdandyvrx7  47230  dandysum2p2e4  47240  or2expropbilem1  47274  dfnelbr2  47515  2ltceilhalf  47570  ich2exprop  47713  paireqne  47753  fmtno4prmfac  47814  31prm  47839  lighneallem4a  47850  41prothprmlem2  47860  zofldiv2ALTV  47904  nfermltl8rev  47984  nfermltl2rev  47985  nfermltlrev  47986  gbegt5  48003  gbowgt5  48004  gboge9  48006  9gbo  48016  11gbo  48017  nnsum3primes4  48030  nnsum3primesgbe  48034  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  tgblthelfgott  48057  tgoldbach  48059  ushggricedg  48169  isubgrgrim  48171  stgrvtx  48196  stgriedg  48197  stgrusgra  48201  stgr1  48203  uspgrlim  48234  grlimprclnbgrvtx  48241  clnbgr3stgrgrlic  48262  usgrexmpl1lem  48263  usgrexmpl2lem  48268  usgrexmpl2nb0  48273  usgrexmpl2nb1  48274  usgrexmpl2nb2  48275  usgrexmpl2nb3  48276  usgrexmpl2nb4  48277  usgrexmpl2nb5  48278  gpgvtx  48285  gpgiedg  48286  gpgorder  48301  gpgvtxedg0  48305  gpgvtxedg1  48306  gpgedgiov  48307  gpg5nbgrvtx03starlem1  48310  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx03starlem3  48312  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem2  48314  gpg5nbgrvtx13starlem3  48315  gpg3kgrtriexlem3  48327  gpg3kgrtriexlem6  48330  gpgprismgr4cycllem2  48338  gpgprismgr4cyclex  48349  pgnioedg1  48350  pgnioedg2  48351  pgnioedg3  48352  pgnioedg4  48353  pgnioedg5  48354  pgnbgreunbgrlem2lem1  48356  pgnbgreunbgrlem2lem2  48357  pgnbgreunbgrlem2lem3  48358  pgnbgreunbgrlem3  48360  pgnbgreunbgrlem4  48361  pgnbgreunbgrlem5lem1  48362  pgnbgreunbgrlem5lem2  48363  pgnbgreunbgrlem5lem3  48364  pgnbgreunbgrlem6  48366  gpg5ngric  48370  gpg5edgnedg  48372  nn0mnd  48421  mgmplusgiopALT  48436  sgrp2sgrp  48470  2zrngaabl  48492  funcringcsetcALTV2lem8  48539  funcringcsetclem8ALTV  48562  zlmodzxzlmod  48596  zlmodzxzel  48597  zlmodzxzscm  48599  zlmodzxzadd  48600  snlindsntorlem  48712  ldepspr  48715  lmod1lem2  48730  lmod1lem3  48731  lmod1lem4  48732  lmod1lem5  48733  lmodn0  48737  zlmodzxznm  48739  zlmodzxzldeplem  48740  zlmodzxzldeplem1  48742  zlmodzxzldeplem3  48744  lvecpsslmod  48749  ldepsnlinc  48750  ldepslinc  48751  expnegico01  48760  zofldiv2  48773  flnn0div2ge  48775  elbigo2  48794  nnlog2ge0lt1  48808  digfval  48839  dignnld  48845  dignn0flhalf  48860  2arymaptfo  48896  itcovalt2lem1  48917  prelrrx2  48955  eenglngeehlnmlem2  48980  rrxsphere  48990  line2  48994  line2x  48996  line2y  48997  itsclc0yqsollem2  49005  inlinecirc02plem  49028  sepfsepc  49169  invfn  49271  alimp-surprise  50021  aacllem  50042