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  694  pm4.87  844  3pm3.2i  1341  unssi  4131  ssini  4180  opthhausdorff  5471  elvv  5706  elopaelxp  5721  relopabiv  5776  relopabi  5778  dfpo2  6260  funpr  6554  funcnvpr  6560  mpov  7479  caovcom  7564  snnex  7712  pwnex  7713  1st2val  7970  2nd2val  7971  elxp7  7977  opreuopreu  7987  poxp2  8093  poseq  8108  tfr1a  8333  oeoa  8533  oeoe  8535  erov  8761  endisj  9002  snopfsupp  9304  ssttrcl  9636  ttrclselem2  9647  r1funlim  9690  dfac2b  10053  cflecard  10175  canth4  10570  canthnumlem  10571  canthwelem  10573  canthp1lem2  10576  pwfseqlem4  10585  wunex3  10664  addsrpr  10998  mulsrpr  10999  recexsrlem  11026  mulcani  11789  div1  11844  recdiv  11861  divdiv1  11866  divdiv2  11867  div23i  11913  div11i  11914  divmuldivi  11915  divadddivi  11917  divdivdivi  11918  lemulge11  12018  negiso  12136  dfnn3  12188  2cnne0  12386  2rene0  12387  halfpm6th  12399  avglt1  12415  avglt2  12416  div4p1lem1div2  12432  3halfnz  12608  divlt1lt  13013  divle1le  13014  nnledivrp  13056  x2times  13251  xrsupsslem  13259  xrinfmsslem  13260  nnge2recico01  13460  fvf1tp  13748  om2uzoi  13917  fzennn  13930  expge1  14061  sqoddm1div8  14205  faclbnd2  14253  faclbnd4lem1  14255  4bc2eq6  14291  hashfxnn0  14299  hashsnlei  14380  hashunlei  14387  hashsslei  14388  hash2prb  14434  repswccat  14748  funcnvs4  14877  f1oun2prg  14879  wrdlen2i  14904  s2rn  14925  s3rn  14926  s7rn  14927  relexpaddg  15015  cjreb  15085  sqrt2gt1lt2  15236  abs1m  15298  bpoly3  16023  ege2le3  16055  efi4p  16104  efival  16119  sin01bnd  16152  cos01bnd  16153  cos1bnd  16154  cos2bnd  16155  sin01gt0  16157  cos01gt0  16158  sin02gt0  16159  sincos2sgn  16161  sin4lt0  16162  egt2lt3  16173  rpnnen2lem3  16183  rpnnen2lem11  16191  nthruc  16219  nthruz  16220  3dvdsdec  16301  3dvds2dec  16302  mod2eq1n2dvds  16316  halfleoddlt  16331  divalglem5  16366  ndvdsi  16381  flodddiv4  16384  flodddiv4lt  16386  bitsp1o  16402  3lcm2e6woprm  16584  6lcm4e12  16585  pcrec  16829  prmrec  16893  prmgaplcmlem1  17022  prmgaplcm  17031  modsubi  17043  structfn  17126  strleun  17127  slotsdifipndx  17298  slotsdifplendx  17338  slotsdifdsndx  17357  slotsdifunifndx  17364  slotsdifplendx2  17379  slotsdifocndx  17380  isofn  17742  sscres  17790  funcestrcsetclem7  18112  funcestrcsetclem8  18113  fullestrcsetc  18117  nulchn  18585  chninf  18601  mgmnsgrpex  18902  pwmnd  18908  ga0  19273  symg2bas  19368  f1otrspeq  19422  psgnsn  19495  0frgp  19754  gsummptnn0fz  19961  srgbinomlem4  20210  isrnghm  20421  rnghmsscmap2  20606  rnghmsscmap  20607  funcrngcsetc  20617  funcrngcsetcALT  20618  rhmsscmap2  20635  rhmsscmap  20636  funcringcsetc  20651  cnfldfun  21366  cnfldfunALT  21367  cnfld1  21377  cnsubdrglem  21398  expmhm  21416  expghm  21455  pzriprnglem4  21464  pzriprnglem9  21469  pzriprnglem14  21474  pzriprng1ALT  21476  psrbag0  22040  psrbagsn  22041  coe1fsupp  22178  coe1mul2  22234  evls1sca  22288  matmulr  22403  mat1dimelbas  22436  mat1f1o  22443  m2detleib  22596  smadiadetglem1  22636  pmatcollpw3fi1lem2  22752  cpmidpmatlem2  22836  cpmadumatpolylem1  22846  cayhamlem3  22852  cayhamlem4  22853  isbasis3g  22914  fctop  22969  cctop  22971  refref  23478  bl2in  24365  dscmet  24537  iihalf1  24898  iihalf2  24900  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  iscvsi  25096  zclmncvs  25115  ncvs1  25124  ehl2eudis  25389  minveclem2  25393  minveclem4  25399  ovolunlem1a  25463  volf  25496  i1f1lem  25656  mbfi1fseqlem5  25686  dveflem  25946  pilem2  26417  pilem3  26418  sinhalfpilem  26427  sincosq1lem  26461  tangtx  26469  sinq12gt0  26471  sincos4thpi  26477  sincos6thpi  26480  sincos3rdpi  26481  pigt3  26482  pige3ALT  26484  coseq1  26489  efeq1  26492  efif1olem4  26509  angneg  26767  ang180lem1  26773  1cubrlem  26805  quart1  26820  log2cnv  26908  log2tlbnd  26909  log2ublem1  26910  log2ub  26913  emcllem1  26959  emcllem6  26964  basellem1  27044  basellem2  27045  basellem3  27046  basellem8  27051  ppiublem1  27165  ppiublem2  27166  ppiub  27167  chtublem  27174  chtub  27175  bcmono  27240  bclbnd  27243  bpos1lem  27245  bposlem1  27247  bposlem2  27248  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem7  27253  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  1lgs  27303  gausslemma2dlem0c  27321  gausslemma2dlem0d  27322  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem3  27331  gausslemma2dlem5  27334  gausslemma2dlem6  27335  lgsquad2lem2  27348  2lgslem1a1  27352  2lgslem1a2  27353  2lgslem1c  27356  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgslem3  27367  2lgsoddprmlem1  27371  addsqrexnreu  27405  addsqnreup  27406  chebbnd1lem1  27432  chebbnd1lem3  27434  chebbnd1  27435  dchrisum0flblem2  27472  dchrisum0lem1  27479  mulog2sumlem2  27498  selberglem2  27509  chpdifbndlem1  27516  sltssnb  27761  mulscl  28126  ltmuls  28128  divs1  28196  precsexlem8  28206  0reno  28488  1reno  28489  slotsinbpsd  28509  slotslnbpsd  28510  ercgrg  28585  axlowdimlem4  29014  axlowdimlem5  29015  axlowdimlem6  29016  axlowdimlem7  29017  axlowdimlem8  29018  axlowdimlem10  29020  axlowdimlem11  29021  graop  29098  grastruct  29099  uhgrunop  29144  upgrop  29163  upgrunop  29188  umgrunop  29190  usgrop  29232  usgr2v1e2w  29321  usgrexmpldifpr  29327  usgrexmpledg  29331  uhgrsubgrself  29349  uhgrspan1lem1  29369  upgrres1lem1  29378  fusgrfis  29399  vtxd0nedgb  29557  p1evtxdeqlem  29581  p1evtxdeq  29582  p1evtxdp1  29583  umgr2v2e  29594  vdegp1bi  29606  wlkcomp  29699  upgr2pthnlp  29800  usgr2trlncl  29828  usgr2pthlem  29831  clwlkcomp  29847  uspgrn2crct  29876  wwlksonvtx  29923  wspthnonp  29927  2wlkond  30005  2pthond  30010  2pthon3v  30011  umgr2adedgwlkonALT  30015  umgr2wlk  30017  umgr2wlkon  30018  wpthswwlks2on  30032  elwspths2spth  30038  0ewlk  30184  0pth  30195  0pthonv  30199  1pthon2v  30223  3wlkdlem4  30232  3trlond  30243  3pthond  30245  3spthond  30247  trlsegvdeglem3  30292  eupthvdres  30305  eupth2lemb  30307  ex-natded5.2i  30476  ex-an  30492  ex-id  30504  ex-po  30505  ex-fl  30517  ex-mod  30519  ex-exp  30520  ex-lcm  30528  nvz0  30739  ipidsq  30781  ipdirilem  30900  siilem1  30922  minvecolem2  30946  minvecolem3  30947  minvecolem4  30951  hvsubcan  31145  hvsubcan2  31146  normlem7tALT  31190  helch  31314  hsn0elch  31319  hhshsslem2  31339  hhsssh  31340  shscli  31388  shintcli  31400  shintcl  31401  chintcli  31402  chintcl  31403  shincli  31433  shsval2i  31458  omlsi  31475  chincli  31531  chabs1  31587  fh1i  31692  fh2i  31693  cm2ji  31696  pjnormi  31792  nmopsetn0  31936  nmfnsetn0  31949  lnophm  32090  nmcexi  32097  nmbdfnlb  32121  imaelshi  32129  nlelshi  32131  nmopadjlem  32160  nmopcoadji  32172  hmopidmch  32224  hmopidmpj  32225  sto1i  32307  stlei  32311  stji1i  32313  csmdsymi  32405  chirred  32466  cdj3lem1  32505  rpdp2cl  32941  dp2lt10  32943  dp2lt  32944  dp2ltc  32946  dpfrac1  32951  dplti  32964  dpgti  32965  dpexpp1  32967  dpadd3  32971  dpmul  32972  dpmul4  32973  xrsclat  33071  nn0archi  33407  zringfrac  33614  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  cos9thpinconstr  33935  lmatfvlem  33959  xrge0iifmhm  34083  qqh0  34128  qqh1  34129  rerrext  34153  cnrrext  34154  prsiga  34275  oms0  34441  coinfliprv  34627  ballotlem1  34631  ballotth  34682  signsw0g  34700  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  tgoldbachgt  34807  subfacval2  35369  erdszelem2  35374  cvmliftlem4  35470  satom  35538  satfv1  35545  sat1el2xp  35561  fmlaomn0  35572  satfdmfmla  35582  satfv1fvfmla1  35605  ex-sategoelelomsuc  35608  ex-sategoelel12  35609  prv0  35612  prv1n  35613  elmrsubrn  35702  msubfval  35706  problem4  35850  quad3  35852  br6  35939  dfon2lem3  35965  fullfunfnv  36128  itgeq12i  36388  fneref  36532  filnetlem2  36561  filnetlem3  36562  onpsstopbas  36612  dfttc3gw  36705  dfttc4lem2  36711  dnizeq0  36735  dnibndlem12  36749  knoppcnlem5  36757  knoppcnlem8  36760  knoppcnlem11  36763  knoppndvlem14  36785  cnndvlem1  36797  bj-genr  36872  bj-genl  36873  bj-genan  36874  bj-2upln1upl  37331  bj-vtoclgfALT  37366  bj-brab2a1  37463  bj-opabssvv  37464  taupilem1  37635  qdiff  37641  topdifinf  37665  sin2h  37931  cos2h  37932  tan2h  37933  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem29  37970  poimirlem31  37972  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  itg2addnclem2  37993  asindmre  38024  heiborlem7  38138  riscer  38309  refrelcoss3  38874  symrelcoss3  38876  ishlatiN  39801  0psubN  40195  atpsubN  40199  gcdcomnni  42427  gcdnegnni  42428  neggcdnni  42429  60gcd7e1  42444  lcmeprodgcdi  42446  lcm2un  42453  lcm3un  42454  lcmineqlem4  42471  lcmineqlem6  42473  3lexlogpow5ineq1  42493  aks4d1p1p2  42509  mzpclall  43159  diophin  43204  diophun  43205  eldioph4b  43239  irrapx1  43256  2nn0ind  43373  aomclem4  43485  onexlimgt  43671  nnoeomeqom  43740  oaomoencom  43745  oenassex  43746  succlg  43756  dflim5  43757  omabs2  43760  tfsconcatfv2  43768  ifpid3g  43919  ifpid2g  43920  ifpbi1b  43930  eu0  43947  pwinfi  43991  rtrclex  44044  cnvrcl0  44052  dfrcl2  44101  relexp1idm  44141  relexp0idm  44142  clsk1independent  44473  lhe4.4ex1a  44756  expgrowth  44762  ax6e2nd  44985  uun0.1  45204  relopabVD  45327  ax6e2ndVD  45334  sb5ALTVD  45339  ax6e2ndALT  45356  permaxinf2lem  45439  rexanuz2nf  45920  dvmptconst  46343  dvmptidg  46345  dvmulcncf  46353  dvdivcncf  46355  dvnprodlem3  46376  itgsinexplem1  46382  volioof  46415  stoweidlem13  46441  stoweidlem14  46442  stoweidlem26  46454  stoweidlem34  46462  stoweidlem49  46477  stoweidlem59  46487  dirkertrigeqlem3  46528  dirkercncflem1  46531  dirkercncflem2  46532  fourierdlem57  46591  fourierdlem62  46596  fourierdlem103  46637  fourierdlem111  46645  fourierswlem  46658  fouriersw  46659  salexct2  46767  salexct3  46770  salgencntex  46771  salgensscntex  46772  gsumge0cl  46799  sge00  46804  sge0tsms  46808  0ome  46957  ovnlecvr  46986  ovn0lem  46993  hoidmvle  47028  ovnsubadd2lem  47073  smflimlem6  47204  mbfpsssmf  47211  smfmullem4  47222  smfpimbor1lem1  47226  nthrucw  47316  goldratmolem2  47334  cjnpoly  47337  sinnpoly  47339  astbstanbst  47357  aistbistaandb  47358  abnotataxb  47364  aifftbifffaibif  47369  confun4  47390  plcofph  47392  plvcofph  47394  plvcofphax  47395  plvofpos  47396  mdandyv0  47397  mdandyv1  47398  mdandyv2  47399  mdandyv3  47400  mdandyv4  47401  mdandyv5  47402  mdandyv6  47403  mdandyv7  47404  mdandyv8  47405  mdandyv9  47406  mdandyv10  47407  mdandyv11  47408  mdandyv12  47409  mdandyv13  47410  mdandyv14  47411  mdandyv15  47412  mdandyvr0  47413  mdandyvr1  47414  mdandyvr2  47415  mdandyvr3  47416  mdandyvr4  47417  mdandyvr5  47418  mdandyvr6  47419  mdandyvr7  47420  mdandyvrx0  47429  mdandyvrx1  47430  mdandyvrx2  47431  mdandyvrx3  47432  mdandyvrx4  47433  mdandyvrx5  47434  mdandyvrx6  47435  mdandyvrx7  47436  dandysum2p2e4  47446  or2expropbilem1  47480  dfnelbr2  47721  2ltceilhalf  47780  flmrecm1  47791  ich2exprop  47931  paireqne  47971  fmtno4prmfac  48035  31prm  48060  lighneallem4a  48071  41prothprmlem2  48081  ppivalnn4  48090  zofldiv2ALTV  48138  nfermltl8rev  48218  nfermltl2rev  48219  nfermltlrev  48220  gbegt5  48237  gbowgt5  48238  gboge9  48240  9gbo  48250  11gbo  48251  nnsum3primes4  48264  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  tgblthelfgott  48291  tgoldbach  48293  ushggricedg  48403  isubgrgrim  48405  stgrvtx  48430  stgriedg  48431  stgrusgra  48435  stgr1  48437  uspgrlim  48468  grlimprclnbgrvtx  48475  clnbgr3stgrgrlic  48496  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  gpgvtx  48519  gpgiedg  48520  gpgorder  48535  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedgiov  48541  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg3kgrtriexlem3  48561  gpg3kgrtriexlem6  48564  gpgprismgr4cycllem2  48572  gpgprismgr4cyclex  48583  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  pgnbgreunbgrlem6  48600  gpg5ngric  48604  gpg5edgnedg  48606  nn0mnd  48655  mgmplusgiopALT  48670  sgrp2sgrp  48704  2zrngaabl  48726  funcringcsetcALTV2lem8  48773  funcringcsetclem8ALTV  48796  zlmodzxzlmod  48830  zlmodzxzel  48831  zlmodzxzscm  48833  zlmodzxzadd  48834  snlindsntorlem  48946  ldepspr  48949  lmod1lem2  48964  lmod1lem3  48965  lmod1lem4  48966  lmod1lem5  48967  lmodn0  48971  zlmodzxznm  48973  zlmodzxzldeplem  48974  zlmodzxzldeplem1  48976  zlmodzxzldeplem3  48978  lvecpsslmod  48983  ldepsnlinc  48984  ldepslinc  48985  expnegico01  48994  zofldiv2  49007  flnn0div2ge  49009  elbigo2  49028  nnlog2ge0lt1  49042  digfval  49073  dignnld  49079  dignn0flhalf  49094  2arymaptfo  49130  itcovalt2lem1  49151  prelrrx2  49189  eenglngeehlnmlem2  49214  rrxsphere  49224  line2  49228  line2x  49230  line2y  49231  itsclc0yqsollem2  49239  inlinecirc02plem  49262  sepfsepc  49403  invfn  49505  alimp-surprise  50255  aacllem  50276