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  4144  ssini  4193  opthhausdorff  5464  elvv  5698  elopaelxp  5713  relopabiv  5767  relopabi  5769  dfpo2  6248  funpr  6542  funcnvpr  6548  mpov  7465  caovcom  7550  snnex  7698  pwnex  7699  1st2val  7959  2nd2val  7960  elxp7  7966  opreuopreu  7976  poxp2  8083  poseq  8098  tfr1a  8323  oeoa  8522  oeoe  8524  erov  8748  endisj  8988  snopfsupp  9300  ssttrcl  9630  ttrclselem2  9641  r1funlim  9681  dfac2b  10044  cflecard  10166  canth4  10560  canthnumlem  10561  canthwelem  10563  canthp1lem2  10566  pwfseqlem4  10575  wunex3  10654  addsrpr  10988  mulsrpr  10989  recexsrlem  11016  mulcani  11777  div1  11832  recdiv  11848  divdiv1  11853  divdiv2  11854  div23i  11900  div11i  11901  divmuldivi  11902  divadddivi  11904  divdivdivi  11905  lemulge11  12005  negiso  12123  dfnn3  12160  2cnne0  12351  2rene0  12352  halfpm6th  12364  avglt1  12380  avglt2  12381  div4p1lem1div2  12397  3halfnz  12573  divlt1lt  12982  divle1le  12983  nnledivrp  13025  x2times  13219  xrsupsslem  13227  xrinfmsslem  13228  fvf1tp  13711  om2uzoi  13880  fzennn  13893  expge1  14024  sqoddm1div8  14168  faclbnd2  14216  faclbnd4lem1  14218  4bc2eq6  14254  hashfxnn0  14262  hashsnlei  14343  hashunlei  14350  hashsslei  14351  hash2prb  14397  repswccat  14710  cshwsexaOLD  14749  funcnvs4  14840  f1oun2prg  14842  wrdlen2i  14867  s2rn  14888  s3rn  14889  s7rn  14890  relexpaddg  14978  cjreb  15048  sqrt2gt1lt2  15199  abs1m  15261  bpoly3  15983  ege2le3  16015  efi4p  16064  efival  16079  sin01bnd  16112  cos01bnd  16113  cos1bnd  16114  cos2bnd  16115  sin01gt0  16117  cos01gt0  16118  sin02gt0  16119  sincos2sgn  16121  sin4lt0  16122  egt2lt3  16133  rpnnen2lem3  16143  rpnnen2lem11  16151  nthruc  16179  nthruz  16180  3dvdsdec  16261  3dvds2dec  16262  mod2eq1n2dvds  16276  halfleoddlt  16291  divalglem5  16326  ndvdsi  16341  flodddiv4  16344  flodddiv4lt  16346  bitsp1o  16362  3lcm2e6woprm  16544  6lcm4e12  16545  pcrec  16788  prmrec  16852  prmgaplcmlem1  16981  prmgaplcm  16990  modsubi  17002  structfn  17085  strleun  17086  slotsdifipndx  17257  slotsdifplendx  17297  slotsdifdsndx  17316  slotsdifunifndx  17323  slotsdifplendx2  17338  slotsdifocndx  17339  isofn  17700  sscres  17748  funcestrcsetclem7  18070  funcestrcsetclem8  18071  fullestrcsetc  18075  mgmnsgrpex  18823  pwmnd  18829  ga0  19195  symg2bas  19290  f1otrspeq  19344  psgnsn  19417  0frgp  19676  gsummptnn0fz  19883  srgbinomlem4  20132  isrnghm  20344  rnghmsscmap2  20532  rnghmsscmap  20533  funcrngcsetc  20543  funcrngcsetcALT  20544  rhmsscmap2  20561  rhmsscmap  20562  funcringcsetc  20577  cnfldfun  21293  cnfldfunALT  21294  cnfldfunOLD  21306  cnfldfunALTOLD  21307  cnfld1  21318  cnfld1OLD  21319  cnsubdrglem  21343  expmhm  21361  expghm  21400  pzriprnglem4  21409  pzriprnglem9  21414  pzriprnglem14  21419  pzriprng1ALT  21421  psrbag0  21985  psrbagsn  21986  coe1fsupp  22115  coe1mul2  22171  evls1sca  22226  matmulr  22341  mat1dimelbas  22374  mat1f1o  22381  m2detleib  22534  smadiadetglem1  22574  pmatcollpw3fi1lem2  22690  cpmidpmatlem2  22774  cpmadumatpolylem1  22784  cayhamlem3  22790  cayhamlem4  22791  isbasis3g  22852  fctop  22907  cctop  22909  refref  23416  bl2in  24304  dscmet  24476  iihalf1  24841  iihalf2  24844  icopnfhmeo  24857  iccpnfhmeo  24859  xrhmeo  24860  iscvsi  25045  zclmncvs  25064  ncvs1  25073  ehl2eudis  25338  minveclem2  25342  minveclem4  25348  ovolunlem1a  25413  volf  25446  i1f1lem  25606  mbfi1fseqlem5  25636  dveflem  25899  pilem2  26378  pilem3  26379  sinhalfpilem  26388  sincosq1lem  26422  tangtx  26430  sinq12gt0  26432  sincos4thpi  26438  sincos6thpi  26441  sincos3rdpi  26442  pigt3  26443  pige3ALT  26445  coseq1  26450  efeq1  26453  efif1olem4  26470  angneg  26729  ang180lem1  26735  1cubrlem  26767  quart1  26782  log2cnv  26870  log2tlbnd  26871  log2ublem1  26872  log2ub  26875  emcllem1  26922  emcllem6  26927  basellem1  27007  basellem2  27008  basellem3  27009  basellem8  27014  ppiublem1  27129  ppiublem2  27130  ppiub  27131  chtublem  27138  chtub  27139  bcmono  27204  bclbnd  27207  bpos1lem  27209  bposlem1  27211  bposlem2  27212  bposlem3  27213  bposlem4  27214  bposlem5  27215  bposlem6  27216  bposlem7  27217  bposlem8  27218  bposlem9  27219  lgsdir2lem1  27252  1lgs  27267  gausslemma2dlem0c  27285  gausslemma2dlem0d  27286  gausslemma2dlem1a  27292  gausslemma2dlem2  27294  gausslemma2dlem3  27295  gausslemma2dlem5  27298  gausslemma2dlem6  27299  lgsquad2lem2  27312  2lgslem1a1  27316  2lgslem1a2  27317  2lgslem1c  27320  2lgslem3a  27323  2lgslem3b  27324  2lgslem3c  27325  2lgslem3d  27326  2lgslem3  27331  2lgsoddprmlem1  27335  addsqrexnreu  27369  addsqnreup  27370  chebbnd1lem1  27396  chebbnd1lem3  27398  chebbnd1  27399  dchrisum0flblem2  27436  dchrisum0lem1  27443  mulog2sumlem2  27462  selberglem2  27473  chpdifbndlem1  27480  mulscl  28060  sltmul  28062  divs1  28130  precsexlem8  28139  0reno  28384  slotsinbpsd  28404  slotslnbpsd  28405  ercgrg  28480  axlowdimlem4  28908  axlowdimlem5  28909  axlowdimlem6  28910  axlowdimlem7  28911  axlowdimlem8  28912  axlowdimlem10  28914  axlowdimlem11  28915  graop  28992  grastruct  28993  uhgrunop  29038  upgrop  29057  upgrunop  29082  umgrunop  29084  usgrop  29126  usgr2v1e2w  29215  usgrexmpldifpr  29221  usgrexmpledg  29225  uhgrsubgrself  29243  uhgrspan1lem1  29263  upgrres1lem1  29272  fusgrfis  29293  vtxd0nedgb  29452  p1evtxdeqlem  29476  p1evtxdeq  29477  p1evtxdp1  29478  umgr2v2e  29489  vdegp1bi  29501  wlkcomp  29594  upgr2pthnlp  29695  usgr2trlncl  29723  usgr2pthlem  29726  clwlkcomp  29742  uspgrn2crct  29771  wwlksonvtx  29818  wspthnonp  29822  2wlkond  29900  2pthond  29905  2pthon3v  29906  umgr2adedgwlkonALT  29910  umgr2wlk  29912  umgr2wlkon  29913  wpthswwlks2on  29924  elwspths2spth  29930  0ewlk  30076  0pth  30087  0pthonv  30091  1pthon2v  30115  3wlkdlem4  30124  3trlond  30135  3pthond  30137  3spthond  30139  trlsegvdeglem3  30184  eupthvdres  30197  eupth2lemb  30199  ex-natded5.2i  30368  ex-an  30384  ex-id  30396  ex-po  30397  ex-fl  30409  ex-mod  30411  ex-exp  30412  ex-lcm  30420  nvz0  30630  ipidsq  30672  ipdirilem  30791  siilem1  30813  minvecolem2  30837  minvecolem3  30838  minvecolem4  30842  hvsubcan  31036  hvsubcan2  31037  normlem7tALT  31081  helch  31205  hsn0elch  31210  hhshsslem2  31230  hhsssh  31231  shscli  31279  shintcli  31291  shintcl  31292  chintcli  31293  chintcl  31294  shincli  31324  shsval2i  31349  omlsi  31366  chincli  31422  chabs1  31478  fh1i  31583  fh2i  31584  cm2ji  31587  pjnormi  31683  nmopsetn0  31827  nmfnsetn0  31840  lnophm  31981  nmcexi  31988  nmbdfnlb  32012  imaelshi  32020  nlelshi  32022  nmopadjlem  32051  nmopcoadji  32063  hmopidmch  32115  hmopidmpj  32116  sto1i  32198  stlei  32202  stji1i  32204  csmdsymi  32296  chirred  32357  cdj3lem1  32396  rpdp2cl  32835  dp2lt10  32837  dp2lt  32838  dp2ltc  32840  dpfrac1  32845  dplti  32858  dpgti  32859  dpexpp1  32861  dpadd3  32865  dpmul  32866  dpmul4  32867  xrsclat  32978  nn0archi  33294  zringfrac  33501  cos9thpiminplylem4  33751  cos9thpiminplylem5  33752  cos9thpinconstr  33757  lmatfvlem  33781  xrge0iifmhm  33905  qqh0  33950  qqh1  33951  rerrext  33975  cnrrext  33976  prsiga  34097  oms0  34264  coinfliprv  34450  ballotlem1  34454  ballotth  34505  signsw0g  34523  hgt750lemd  34615  hgt750lem  34618  hgt750lem2  34619  hgt750leme  34625  tgoldbachgt  34630  subfacval2  35159  erdszelem2  35164  cvmliftlem4  35260  satom  35328  satfv1  35335  sat1el2xp  35351  fmlaomn0  35362  satfdmfmla  35372  satfv1fvfmla1  35395  ex-sategoelelomsuc  35398  ex-sategoelel12  35399  prv0  35402  prv1n  35403  elmrsubrn  35492  msubfval  35496  problem4  35640  quad3  35642  br6  35729  dfon2lem3  35758  fullfunfnv  35919  itgeq12i  36179  fneref  36323  filnetlem2  36352  filnetlem3  36353  onpsstopbas  36403  dnizeq0  36448  dnibndlem12  36462  knoppcnlem5  36470  knoppcnlem8  36473  knoppcnlem11  36476  knoppndvlem14  36498  cnndvlem1  36510  bj-genr  36579  bj-genl  36580  bj-genan  36581  bj-2upln1upl  36997  bj-vtoclgfALT  37032  bj-brab2a1  37122  bj-opabssvv  37123  taupilem1  37294  topdifinf  37322  sin2h  37589  cos2h  37590  tan2h  37591  poimirlem1  37600  poimirlem2  37601  poimirlem3  37602  poimirlem4  37603  poimirlem6  37605  poimirlem7  37606  poimirlem11  37610  poimirlem12  37611  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem22  37621  poimirlem23  37622  poimirlem24  37623  poimirlem25  37624  poimirlem26  37625  poimirlem29  37628  poimirlem31  37630  mblfinlem3  37638  mblfinlem4  37639  ismblfin  37640  itg2addnclem2  37651  asindmre  37682  heiborlem7  37796  riscer  37967  refrelcoss3  38439  symrelcoss3  38441  ishlatiN  39333  0psubN  39728  atpsubN  39732  gcdcomnni  41961  gcdnegnni  41962  neggcdnni  41963  60gcd7e1  41978  lcmeprodgcdi  41980  lcm2un  41987  lcm3un  41988  lcmineqlem4  42005  lcmineqlem6  42007  3lexlogpow5ineq1  42027  aks4d1p1p2  42043  mzpclall  42700  diophin  42745  diophun  42746  eldioph4b  42784  irrapx1  42801  2nn0ind  42918  aomclem4  43030  onexlimgt  43216  nnoeomeqom  43285  oaomoencom  43290  oenassex  43291  succlg  43301  dflim5  43302  omabs2  43305  tfsconcatfv2  43313  ifpid3g  43465  ifpid2g  43466  ifpbi1b  43476  eu0  43493  pwinfi  43537  rtrclex  43590  cnvrcl0  43598  dfrcl2  43647  relexp1idm  43687  relexp0idm  43688  clsk1independent  44019  lhe4.4ex1a  44302  expgrowth  44308  ax6e2nd  44532  uun0.1  44751  relopabVD  44874  ax6e2ndVD  44881  sb5ALTVD  44886  ax6e2ndALT  44903  permaxinf2lem  44986  rexanuz2nf  45472  dvmptconst  45897  dvmptidg  45899  dvmulcncf  45907  dvdivcncf  45909  dvnprodlem3  45930  itgsinexplem1  45936  volioof  45969  stoweidlem13  45995  stoweidlem14  45996  stoweidlem26  46008  stoweidlem34  46016  stoweidlem49  46031  stoweidlem59  46041  dirkertrigeqlem3  46082  dirkercncflem1  46085  dirkercncflem2  46086  fourierdlem57  46145  fourierdlem62  46150  fourierdlem103  46191  fourierdlem111  46199  fourierswlem  46212  fouriersw  46213  salexct2  46321  salexct3  46324  salgencntex  46325  salgensscntex  46326  gsumge0cl  46353  sge00  46358  sge0tsms  46362  0ome  46511  ovnlecvr  46540  ovn0lem  46547  hoidmvle  46582  ovnsubadd2lem  46627  smflimlem6  46758  mbfpsssmf  46765  smfmullem4  46776  smfpimbor1lem1  46780  cjnpoly  46874  sinnpoly  46876  astbstanbst  46894  aistbistaandb  46895  abnotataxb  46901  aifftbifffaibif  46906  confun4  46927  plcofph  46929  plvcofph  46931  plvcofphax  46932  plvofpos  46933  mdandyv0  46934  mdandyv1  46935  mdandyv2  46936  mdandyv3  46937  mdandyv4  46938  mdandyv5  46939  mdandyv6  46940  mdandyv7  46941  mdandyv8  46942  mdandyv9  46943  mdandyv10  46944  mdandyv11  46945  mdandyv12  46946  mdandyv13  46947  mdandyv14  46948  mdandyv15  46949  mdandyvr0  46950  mdandyvr1  46951  mdandyvr2  46952  mdandyvr3  46953  mdandyvr4  46954  mdandyvr5  46955  mdandyvr6  46956  mdandyvr7  46957  mdandyvrx0  46966  mdandyvrx1  46967  mdandyvrx2  46968  mdandyvrx3  46969  mdandyvrx4  46970  mdandyvrx5  46971  mdandyvrx6  46972  mdandyvrx7  46973  dandysum2p2e4  46983  or2expropbilem1  47017  dfnelbr2  47258  2ltceilhalf  47313  ich2exprop  47456  paireqne  47496  fmtno4prmfac  47557  31prm  47582  lighneallem4a  47593  41prothprmlem2  47603  zofldiv2ALTV  47647  nfermltl8rev  47727  nfermltl2rev  47728  nfermltlrev  47729  gbegt5  47746  gbowgt5  47747  gboge9  47749  9gbo  47759  11gbo  47760  nnsum3primes4  47773  nnsum3primesgbe  47777  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  tgblthelfgott  47800  tgoldbach  47802  ushggricedg  47912  isubgrgrim  47914  stgrvtx  47939  stgriedg  47940  stgrusgra  47944  stgr1  47946  uspgrlim  47977  grlimprclnbgrvtx  47984  clnbgr3stgrgrlic  48005  usgrexmpl1lem  48006  usgrexmpl2lem  48011  usgrexmpl2nb0  48016  usgrexmpl2nb1  48017  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2nb4  48020  usgrexmpl2nb5  48021  gpgvtx  48028  gpgiedg  48029  gpgorder  48044  gpgvtxedg0  48048  gpgvtxedg1  48049  gpgedgiov  48050  gpg5nbgrvtx03starlem1  48053  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx03starlem3  48055  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem2  48057  gpg5nbgrvtx13starlem3  48058  gpg3kgrtriexlem3  48070  gpg3kgrtriexlem6  48073  gpgprismgr4cycllem2  48081  gpgprismgr4cyclex  48092  pgnioedg1  48093  pgnioedg2  48094  pgnioedg3  48095  pgnioedg4  48096  pgnioedg5  48097  pgnbgreunbgrlem2lem1  48099  pgnbgreunbgrlem2lem2  48100  pgnbgreunbgrlem2lem3  48101  pgnbgreunbgrlem3  48103  pgnbgreunbgrlem4  48104  pgnbgreunbgrlem5lem1  48105  pgnbgreunbgrlem5lem2  48106  pgnbgreunbgrlem5lem3  48107  pgnbgreunbgrlem6  48109  gpg5ngric  48113  gpg5edgnedg  48115  nn0mnd  48164  mgmplusgiopALT  48179  sgrp2sgrp  48213  2zrngaabl  48235  funcringcsetcALTV2lem8  48282  funcringcsetclem8ALTV  48305  zlmodzxzlmod  48339  zlmodzxzel  48340  zlmodzxzscm  48342  zlmodzxzadd  48343  snlindsntorlem  48456  ldepspr  48459  lmod1lem2  48474  lmod1lem3  48475  lmod1lem4  48476  lmod1lem5  48477  lmodn0  48481  zlmodzxznm  48483  zlmodzxzldeplem  48484  zlmodzxzldeplem1  48486  zlmodzxzldeplem3  48488  lvecpsslmod  48493  ldepsnlinc  48494  ldepslinc  48495  expnegico01  48504  zofldiv2  48517  flnn0div2ge  48519  elbigo2  48538  nnlog2ge0lt1  48552  digfval  48583  dignnld  48589  dignn0flhalf  48604  2arymaptfo  48640  itcovalt2lem1  48661  prelrrx2  48699  eenglngeehlnmlem2  48724  rrxsphere  48734  line2  48738  line2x  48740  line2y  48741  itsclc0yqsollem2  48749  inlinecirc02plem  48772  sepfsepc  48913  invfn  49016  alimp-surprise  49766  aacllem  49787