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  692  pm4.87  842  3pm3.2i  1339  unssi  4214  ssini  4261  opthhausdorff  5536  elvv  5774  elopaelxp  5789  relopabiv  5844  relopabi  5846  dfpo2  6327  funpr  6634  funcnvpr  6640  mpov  7562  caovcom  7647  snnex  7793  pwnex  7794  1st2val  8058  2nd2val  8059  elxp7  8065  opreuopreu  8075  mptmpoopabbrdOLDOLD  8124  poxp2  8184  poseq  8199  wfrlem13OLD  8377  wfr3OLD  8394  tfr1a  8450  oeoa  8653  oeoe  8655  erov  8872  endisj  9124  phplem2OLD  9281  snopfsupp  9460  ssttrcl  9784  ttrclselem2  9795  r1funlim  9835  dfac2b  10200  cflecard  10322  canth4  10716  canthnumlem  10717  canthwelem  10719  canthp1lem2  10722  pwfseqlem4  10731  wunex3  10810  addsrpr  11144  mulsrpr  11145  recexsrlem  11172  mulcani  11929  div1  11984  recdiv  12000  divdiv1  12005  divdiv2  12006  div23i  12052  div11i  12053  divmuldivi  12054  divadddivi  12056  divdivdivi  12057  lemulge11  12157  negiso  12275  dfnn3  12307  2cnne0  12503  2rene0  12504  halfpm6th  12514  avglt1  12531  avglt2  12532  div4p1lem1div2  12548  3halfnz  12722  divlt1lt  13126  divle1le  13127  nnledivrp  13169  x2times  13361  xrsupsslem  13369  xrinfmsslem  13370  fvf1tp  13840  om2uzoi  14006  fzennn  14019  expge1  14150  sqoddm1div8  14292  faclbnd2  14340  faclbnd4lem1  14342  4bc2eq6  14378  hashfxnn0  14386  hashsnlei  14467  hashunlei  14474  hashsslei  14475  hash2prb  14521  repswccat  14834  cshwsexaOLD  14873  funcnvs4  14964  f1oun2prg  14966  wrdlen2i  14991  s2rn  15012  s3rn  15013  s7rn  15014  relexpaddg  15102  cjreb  15172  sqrt2gt1lt2  15323  abs1m  15384  bpoly3  16106  ege2le3  16138  efi4p  16185  efival  16200  sin01bnd  16233  cos01bnd  16234  cos1bnd  16235  cos2bnd  16236  sin01gt0  16238  cos01gt0  16239  sin02gt0  16240  sincos2sgn  16242  sin4lt0  16243  egt2lt3  16254  rpnnen2lem3  16264  rpnnen2lem11  16272  nthruc  16300  nthruz  16301  3dvdsdec  16380  3dvds2dec  16381  mod2eq1n2dvds  16395  halfleoddlt  16410  divalglem5  16445  ndvdsi  16460  flodddiv4  16461  flodddiv4lt  16463  bitsp1o  16479  3lcm2e6woprm  16662  6lcm4e12  16663  pcrec  16905  prmrec  16969  prmgaplcmlem1  17098  prmgaplcm  17107  modsubi  17119  structfn  17203  strleun  17204  slotsdifipndx  17394  slotsdifplendx  17434  slotsdifdsndx  17453  slotsdifunifndx  17460  slotsdifplendx2  17476  slotsdifocndx  17477  isofn  17836  sscres  17884  funcestrcsetclem7  18215  funcestrcsetclem8  18216  fullestrcsetc  18220  mgmnsgrpex  18966  pwmnd  18972  ga0  19338  symg2bas  19434  f1otrspeq  19489  psgnsn  19562  0frgp  19821  gsummptnn0fz  20028  srgbinomlem4  20256  isrnghm  20467  rnghmsscmap2  20651  rnghmsscmap  20652  funcrngcsetc  20662  funcrngcsetcALT  20663  rhmsscmap2  20680  rhmsscmap  20681  funcringcsetc  20696  cnfldfun  21401  cnfldfunALT  21402  cnfldfunOLD  21414  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  cnfld1  21429  cnfld1OLD  21430  cnsubdrglem  21459  expmhm  21477  expghm  21509  pzriprnglem4  21518  pzriprnglem9  21523  pzriprnglem14  21528  pzriprng1ALT  21530  psrbag0  22109  psrbagsn  22110  coe1fsupp  22237  coe1mul2  22293  evls1sca  22348  matmulr  22465  mat1dimelbas  22498  mat1f1o  22505  m2detleib  22658  smadiadetglem1  22698  pmatcollpw3fi1lem2  22814  cpmidpmatlem2  22898  cpmadumatpolylem1  22908  cayhamlem3  22914  cayhamlem4  22915  isbasis3g  22977  fctop  23032  cctop  23034  refref  23542  bl2in  24431  dscmet  24606  iihalf1  24977  iihalf2  24980  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  iscvsi  25181  zclmncvs  25201  ncvs1  25210  ehl2eudis  25475  minveclem2  25479  minveclem4  25485  ovolunlem1a  25550  volf  25583  i1f1lem  25743  mbfi1fseqlem5  25774  dveflem  26037  pilem2  26514  pilem3  26515  sinhalfpilem  26523  sincosq1lem  26557  tangtx  26565  sinq12gt0  26567  sincos4thpi  26573  sincos6thpi  26576  sincos3rdpi  26577  pigt3  26578  pige3ALT  26580  coseq1  26585  efeq1  26588  efif1olem4  26605  angneg  26864  ang180lem1  26870  1cubrlem  26902  quart1  26917  log2cnv  27005  log2tlbnd  27006  log2ublem1  27007  log2ub  27010  emcllem1  27057  emcllem6  27062  basellem1  27142  basellem2  27143  basellem3  27144  basellem8  27149  ppiublem1  27264  ppiublem2  27265  ppiub  27266  chtublem  27273  chtub  27274  bcmono  27339  bclbnd  27342  bpos1lem  27344  bposlem1  27346  bposlem2  27347  bposlem3  27348  bposlem4  27349  bposlem5  27350  bposlem6  27351  bposlem7  27352  bposlem8  27353  bposlem9  27354  lgsdir2lem1  27387  1lgs  27402  gausslemma2dlem0c  27420  gausslemma2dlem0d  27421  gausslemma2dlem1a  27427  gausslemma2dlem2  27429  gausslemma2dlem3  27430  gausslemma2dlem5  27433  gausslemma2dlem6  27434  lgsquad2lem2  27447  2lgslem1a1  27451  2lgslem1a2  27452  2lgslem1c  27455  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2lgslem3  27466  2lgsoddprmlem1  27470  addsqrexnreu  27504  addsqnreup  27505  chebbnd1lem1  27531  chebbnd1lem3  27533  chebbnd1  27534  dchrisum0flblem2  27571  dchrisum0lem1  27578  mulog2sumlem2  27597  selberglem2  27608  chpdifbndlem1  27615  mulscl  28178  sltmul  28180  divs1  28247  precsexlem8  28256  nohalf  28425  0reno  28447  slotsinbpsd  28467  slotslnbpsd  28468  ercgrg  28543  axlowdimlem4  28978  axlowdimlem5  28979  axlowdimlem6  28980  axlowdimlem7  28981  axlowdimlem8  28982  axlowdimlem10  28984  axlowdimlem11  28985  graop  29064  grastruct  29065  uhgrunop  29110  upgrop  29129  upgrunop  29154  umgrunop  29156  usgrop  29198  usgr2v1e2w  29287  usgrexmpldifpr  29293  usgrexmpledg  29297  uhgrsubgrself  29315  uhgrspan1lem1  29335  upgrres1lem1  29344  fusgrfis  29365  vtxd0nedgb  29524  p1evtxdeqlem  29548  p1evtxdeq  29549  p1evtxdp1  29550  umgr2v2e  29561  vdegp1bi  29573  wlkcomp  29667  upgr2pthnlp  29768  usgr2trlncl  29796  usgr2pthlem  29799  clwlkcomp  29815  uspgrn2crct  29841  wwlksonvtx  29888  wspthnonp  29892  2wlkond  29970  2pthond  29975  2pthon3v  29976  umgr2adedgwlkonALT  29980  umgr2wlk  29982  umgr2wlkon  29983  wpthswwlks2on  29994  elwspths2spth  30000  0ewlk  30146  0pth  30157  0pthonv  30161  1pthon2v  30185  3wlkdlem4  30194  3trlond  30205  3pthond  30207  3spthond  30209  trlsegvdeglem3  30254  eupthvdres  30267  eupth2lemb  30269  ex-natded5.2i  30438  ex-an  30454  ex-id  30466  ex-po  30467  ex-fl  30479  ex-mod  30481  ex-exp  30482  ex-lcm  30490  nvz0  30700  ipidsq  30742  ipdirilem  30861  siilem1  30883  minvecolem2  30907  minvecolem3  30908  minvecolem4  30912  hvsubcan  31106  hvsubcan2  31107  normlem7tALT  31151  helch  31275  hsn0elch  31280  hhshsslem2  31300  hhsssh  31301  shscli  31349  shintcli  31361  shintcl  31362  chintcli  31363  chintcl  31364  shincli  31394  shsval2i  31419  omlsi  31436  chincli  31492  chabs1  31548  fh1i  31653  fh2i  31654  cm2ji  31657  pjnormi  31753  nmopsetn0  31897  nmfnsetn0  31910  lnophm  32051  nmcexi  32058  nmbdfnlb  32082  imaelshi  32090  nlelshi  32092  nmopadjlem  32121  nmopcoadji  32133  hmopidmch  32185  hmopidmpj  32186  sto1i  32268  stlei  32272  stji1i  32274  csmdsymi  32366  chirred  32427  cdj3lem1  32466  rpdp2cl  32846  dp2lt10  32848  dp2lt  32849  dp2ltc  32851  dpfrac1  32856  dplti  32869  dpgti  32870  dpexpp1  32872  dpadd3  32876  dpmul  32877  dpmul4  32878  xrsclat  32994  nn0archi  33340  zringfrac  33547  lmatfvlem  33761  xrge0iifmhm  33885  qqh0  33930  qqh1  33931  rerrext  33955  cnrrext  33956  prsiga  34095  oms0  34262  coinfliprv  34447  ballotlem1  34451  ballotth  34502  signsw0g  34533  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  tgoldbachgt  34640  subfacval2  35155  erdszelem2  35160  cvmliftlem4  35256  satom  35324  satfv1  35331  sat1el2xp  35347  fmlaomn0  35358  satfdmfmla  35368  satfv1fvfmla1  35391  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  prv0  35398  prv1n  35399  elmrsubrn  35488  msubfval  35492  problem4  35636  quad3  35638  br6  35719  dfon2lem3  35749  fullfunfnv  35910  itgeq12i  36170  fneref  36316  filnetlem2  36345  filnetlem3  36346  onpsstopbas  36396  dnizeq0  36441  dnibndlem12  36455  knoppcnlem5  36463  knoppcnlem8  36466  knoppcnlem11  36469  knoppndvlem14  36491  cnndvlem1  36503  bj-genr  36572  bj-genl  36573  bj-genan  36574  bj-2upln1upl  36990  bj-vtoclgfALT  37025  bj-brab2a1  37115  bj-opabssvv  37116  taupilem1  37287  topdifinf  37315  sin2h  37570  cos2h  37571  tan2h  37572  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem29  37609  poimirlem31  37611  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnclem2  37632  asindmre  37663  heiborlem7  37777  riscer  37948  refrelcoss3  38419  symrelcoss3  38421  ishlatiN  39311  0psubN  39706  atpsubN  39710  gcdcomnni  41945  gcdnegnni  41946  neggcdnni  41947  60gcd7e1  41962  lcmeprodgcdi  41964  lcm2un  41971  lcm3un  41972  lcmineqlem4  41989  lcmineqlem6  41991  3lexlogpow5ineq1  42011  aks4d1p1p2  42027  mzpclall  42683  diophin  42728  diophun  42729  eldioph4b  42767  irrapx1  42784  2nn0ind  42902  aomclem4  43014  onexlimgt  43204  nnoeomeqom  43274  oaomoencom  43279  oenassex  43280  succlg  43290  dflim5  43291  omabs2  43294  tfsconcatfv2  43302  ifpid3g  43454  ifpid2g  43455  ifpbi1b  43465  eu0  43482  pwinfi  43526  rtrclex  43579  cnvrcl0  43587  dfrcl2  43636  relexp1idm  43676  relexp0idm  43677  clsk1independent  44008  lhe4.4ex1a  44298  expgrowth  44304  ax6e2nd  44529  uun0.1  44749  relopabVD  44872  ax6e2ndVD  44879  sb5ALTVD  44884  ax6e2ndALT  44901  rexanuz2nf  45408  dvmptconst  45836  dvmptidg  45838  dvmulcncf  45846  dvdivcncf  45848  dvnprodlem3  45869  itgsinexplem1  45875  volioof  45908  stoweidlem13  45934  stoweidlem14  45935  stoweidlem26  45947  stoweidlem34  45955  stoweidlem49  45970  stoweidlem59  45980  dirkertrigeqlem3  46021  dirkercncflem1  46024  dirkercncflem2  46025  fourierdlem57  46084  fourierdlem62  46089  fourierdlem103  46130  fourierdlem111  46138  fourierswlem  46151  fouriersw  46152  salexct2  46260  salexct3  46263  salgencntex  46264  salgensscntex  46265  gsumge0cl  46292  sge00  46297  sge0tsms  46301  0ome  46450  ovnlecvr  46479  ovn0lem  46486  hoidmvle  46521  ovnsubadd2lem  46566  smflimlem6  46697  mbfpsssmf  46704  smfmullem4  46715  smfpimbor1lem1  46719  astbstanbst  46824  aistbistaandb  46825  abnotataxb  46831  aifftbifffaibif  46836  confun4  46857  plcofph  46859  plvcofph  46861  plvcofphax  46862  plvofpos  46863  mdandyv0  46864  mdandyv1  46865  mdandyv2  46866  mdandyv3  46867  mdandyv4  46868  mdandyv5  46869  mdandyv6  46870  mdandyv7  46871  mdandyv8  46872  mdandyv9  46873  mdandyv10  46874  mdandyv11  46875  mdandyv12  46876  mdandyv13  46877  mdandyv14  46878  mdandyv15  46879  mdandyvr0  46880  mdandyvr1  46881  mdandyvr2  46882  mdandyvr3  46883  mdandyvr4  46884  mdandyvr5  46885  mdandyvr6  46886  mdandyvr7  46887  mdandyvrx0  46896  mdandyvrx1  46897  mdandyvrx2  46898  mdandyvrx3  46899  mdandyvrx4  46900  mdandyvrx5  46901  mdandyvrx6  46902  mdandyvrx7  46903  dandysum2p2e4  46913  or2expropbilem1  46947  dfnelbr2  47188  ich2exprop  47345  paireqne  47385  fmtno4prmfac  47446  31prm  47471  lighneallem4a  47482  41prothprmlem2  47492  zofldiv2ALTV  47536  nfermltl8rev  47616  nfermltl2rev  47617  nfermltlrev  47618  gbegt5  47635  gbowgt5  47636  gboge9  47638  9gbo  47648  11gbo  47649  nnsum3primes4  47662  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  tgblthelfgott  47689  tgoldbach  47691  ushggricedg  47780  isubgrgrim  47781  uspgrlim  47816  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  nn0mnd  47902  mgmplusgiopALT  47917  sgrp2sgrp  47951  2zrngaabl  47973  funcringcsetcALTV2lem8  48020  funcringcsetclem8ALTV  48043  zlmodzxzlmod  48079  zlmodzxzel  48080  zlmodzxzscm  48082  zlmodzxzadd  48083  snlindsntorlem  48199  ldepspr  48202  lmod1lem2  48217  lmod1lem3  48218  lmod1lem4  48219  lmod1lem5  48220  lmodn0  48224  zlmodzxznm  48226  zlmodzxzldeplem  48227  zlmodzxzldeplem1  48229  zlmodzxzldeplem3  48231  lvecpsslmod  48236  ldepsnlinc  48237  ldepslinc  48238  expnegico01  48247  zofldiv2  48265  flnn0div2ge  48267  elbigo2  48286  nnlog2ge0lt1  48300  digfval  48331  dignnld  48337  dignn0flhalf  48352  2arymaptfo  48388  itcovalt2lem1  48409  prelrrx2  48447  eenglngeehlnmlem2  48472  rrxsphere  48482  line2  48486  line2x  48488  line2y  48489  itsclc0yqsollem2  48497  inlinecirc02plem  48520  sepfsepc  48607  alimp-surprise  48874  aacllem  48895