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  6292  funpr  6588  funcnvpr  6594  mpov  7524  caovcom  7610  snnex  7761  pwnex  7762  1st2val  8018  2nd2val  8019  elxp7  8025  opreuopreu  8035  poxp2  8144  poseq  8159  tfr1a  8386  oeoa  8590  oeoe  8592  erov  8819  endisj  9067  snopfsupp  9367  ssttrcl  9700  ttrclselem2  9711  r1funlimOLD  9754  dfac2b  10190  cflecard  10311  canth4  10713  canthnumlem  10714  canthwelem  10716  canthp1lem2  10719  pwfseqlem4  10728  wunex3  10807  addsrpr  11141  mulsrpr  11142  recexsrlem  11169  mulcani  11936  div1  11987  recdiv  12004  divdiv1  12009  divdiv2  12010  div23i  12056  div11i  12057  divmuldivi  12058  divadddivi  12060  divdivdivi  12061  lemulge11  12160  negiso  12278  dfnn3  12330  2cnne0  12536  2rene0  12537  halfpm6th  12549  avglt1  12565  avglt2  12566  div4p1lem1div2  12582  3halfnz  12759  divlt1lt  13172  divle1le  13173  nnledivrp  13215  x2times  13410  xrsupsslem  13418  xrinfmsslem  13419  nnge2recico01  13619  fvf1tp  13909  om2uzoi  14078  fzennn  14091  expge1  14222  sqoddm1div8  14367  faclbnd2  14415  faclbnd4lem1  14417  4bc2eq6  14453  hashfxnn0  14461  hashsnlei  14543  hashunlei  14550  hashsslei  14551  hash2prb  14597  repswccat  14917  funcnvs4  15046  f1oun2prg  15048  wrdlen2i  15073  s2rn  15096  s3rn  15097  s7rn  15098  relexpaddg  15186  cjreb  15270  sqrt2gt1lt2  15421  abs1m  15483  bpoly3  16204  ege2le3  16236  efi4p  16285  efival  16300  sin01bnd  16333  cos01bnd  16334  cos1bnd  16335  cos2bnd  16336  sin01gt0  16338  cos01gt0  16339  sin02gt0  16340  sincos2sgn  16342  sin4lt0  16343  egt2lt3  16354  rpnnen2lem3  16364  rpnnen2lem11  16372  nthruc  16400  nthruz  16401  3dvdsdec  16482  3dvds2dec  16483  mod2eq1n2dvds  16497  halfleoddlt  16512  divalglem5  16547  ndvdsi  16562  flodddiv4  16565  flodddiv4lt  16567  bitsp1o  16583  3lcm2e6woprm  16770  6lcm4e12  16771  pcrec  17016  prmrec  17080  prmgaplcmlem1  17209  prmgaplcm  17218  modsubi  17230  structfn  17314  strleun  17315  slotsdifipndx  17486  slotsdifplendx  17526  slotsdifdsndx  17545  slotsdifunifndx  17552  slotsdifplendx2  17567  slotsdifocndx  17568  isofn  17930  sscres  17978  funcestrcsetclem7  18300  funcestrcsetclem8  18301  fullestrcsetc  18305  nulchn  18773  chninf  18789  mgmnsgrpex  19110  degenmgm  19117  degenmgm2nfun  19119  degenmgm2  19120  pwmnd  19123  ga0  19492  symg2bas  19587  f1otrspeq  19641  psgnsn  19714  0frgp  19973  gsummptnn0fz  20180  srgbinomlem4  20435  isrnghm  20651  rnghmsscmap2  20861  rnghmsscmap  20862  funcrngcsetc  20872  funcrngcsetcALT  20873  rhmsscmap2  20890  rhmsscmap  20891  funcringcsetc  20906  cnfldfun  21672  cnfldfunALT  21673  cnfld1  21683  cnsubdrglem  21704  expmhm  21722  expghm  21761  pzriprnglem4  21770  pzriprnglem9  21775  pzriprnglem14  21780  pzriprng1ALT  21782  psrbag0  22351  psrbagsn  22352  coe1fsupp  22512  coe1mul2  22568  evls1sca  22621  matmulr  22733  mat1dimelbas  22766  mat1f1o  22773  m2detleib  22926  smadiadetglem1  22966  pmatcollpw3fi1lem2  23085  cpmidpmatlem2  23169  cpmadumatpolylem1  23179  cayhamlem3  23185  cayhamlem4  23186  isbasis3g  23247  fctop  23302  cctop  23304  refref  23812  bl2in  24699  dscmet  24871  iihalf1  25232  iihalf2  25234  icopnfhmeo  25244  iccpnfhmeo  25246  xrhmeo  25247  iscvsi  25430  zclmncvs  25449  ncvs1  25458  ehl2eudis  25723  minveclem2  25727  minveclem4  25733  ovolunlem1a  25797  volf  25830  i1f1lem  25990  mbfi1fseqlem5  26020  dveflem  26279  pilem2  26761  pilem3  26762  sinhalfpilem  26774  sincosq1lem  26808  tangtx  26816  sinq12gt0  26818  sincos4thpi  26824  sincos6thpi  26826  sincos3rdpi  26827  pigt3  26828  pige3ALT  26830  coseq1  26835  efeq1  26838  efif1olem4  26855  angneg  27113  ang180lem1  27119  1cubrlem  27151  quart1  27166  log2cnv  27254  log2tlbnd  27255  log2ublem1  27256  log2ub  27259  emcllem1  27305  emcllem6  27310  basellem1  27390  basellem2  27391  basellem3  27392  basellem8  27397  ppiublem1  27511  ppiublem2  27512  ppiub  27513  chtublem  27520  chtub  27521  bcmono  27586  bclbnd  27589  bpos1lem  27591  bposlem1  27593  bposlem2  27594  bposlem3  27595  bposlem4  27596  bposlem5  27597  bposlem6  27598  bposlem7  27599  bposlem8  27600  bposlem9  27601  lgsdir2lem1  27634  1lgs  27649  gausslemma2dlem0c  27667  gausslemma2dlem0d  27668  gausslemma2dlem1a  27674  gausslemma2dlem2  27676  gausslemma2dlem3  27677  gausslemma2dlem5  27680  gausslemma2dlem6  27681  lgsquad2lem2  27694  2lgslem1a1  27698  2lgslem1a2  27699  2lgslem1c  27702  2lgslem3a  27705  2lgslem3b  27706  2lgslem3c  27707  2lgslem3d  27708  2lgslem3  27713  2lgsoddprmlem1  27717  addsqrexnreu  27751  addsqnreup  27752  chebbnd1lem1  27778  chebbnd1lem3  27780  chebbnd1  27781  dchrisum0flblem2  27818  dchrisum0lem1  27825  mulog2sumlem2  27844  selberglem2  27855  chpdifbndlem1  27862  sltssnb  28137  mulscl  28502  ltmuls  28504  divs1  28572  precsexlem8  28582  0reno  28864  1reno  28865  slotsinbpsd  28885  slotslnbpsd  28886  ercgrg  28962  axlowdimlem4  29505  axlowdimlem5  29506  axlowdimlem6  29507  axlowdimlem7  29508  axlowdimlem8  29509  axlowdimlem10  29511  axlowdimlem11  29512  graop  29589  grastruct  29590  uhgrunop  29635  upgrop  29654  upgrunop  29679  umgrunop  29681  usgrop  29726  usgr2v1e2w  29815  usgrexmpldifpr  29821  usgrexmpledg  29825  uhgrsubgrself  29843  uhgrspan1lem1  29863  upgrres1lem1  29872  fusgrfis  29893  vtxd0nedgb  30051  p1evtxdeqlem  30075  p1evtxdeq  30076  p1evtxdp1  30077  umgr2v2e  30088  vdegp1bi  30100  wlkcomp  30193  upgr2pthnlp  30300  usgr2trlncl  30328  usgr2pthlem  30331  clwlkcomp  30348  uspgrn2crct  30379  wwlksonvtx  30426  wspthnonp  30430  2wlkond  30508  2pthond  30513  2pthon3v  30514  umgr2adedgwlkonALT  30518  umgr2wlk  30520  umgr2wlkon  30521  wpthswwlks2on  30535  elwspths2spth  30541  0ewlk  30687  0pth  30698  0pthonv  30702  1pthon2v  30736  3wlkdlem4  30745  3trlond  30756  3pthond  30758  3spthond  30760  trlsegvdeglem3  30805  eupthvdres  30818  eupth2lemb  30820  ex-natded5.2i  30989  ex-an  31005  ex-id  31017  ex-po  31018  ex-fl  31030  ex-mod  31032  ex-exp  31033  ex-lcm  31041  nvz0  31252  ipidsq  31294  ipdirilem  31413  siilem1  31435  minvecolem2  31459  minvecolem3  31460  minvecolem4  31464  hvsubcan  31658  hvsubcan2  31659  normlem7tALT  31703  helch  31827  hsn0elch  31832  hhshsslem2  31852  hhsssh  31853  shscli  31901  shintcli  31913  shintcl  31914  chintcli  31915  chintcl  31916  shincli  31946  shsval2i  31971  omlsi  31988  chincli  32044  chabs1  32100  fh1i  32205  fh2i  32206  cm2ji  32209  pjnormi  32305  nmopsetn0  32449  nmfnsetn0  32462  lnophm  32603  nmcexi  32610  nmbdfnlb  32634  imaelshi  32642  nlelshi  32644  nmopadjlem  32673  nmopcoadji  32685  hmopidmch  32737  hmopidmpj  32738  sto1i  32820  stlei  32824  stji1i  32826  csmdsymi  32918  chirred  32979  cdj3lem1  33018  rpdp2cl  33430  dp2lt10  33432  dp2lt  33433  dp2ltc  33435  dpfrac1  33440  dplti  33453  dpgti  33454  dpexpp1  33456  dpadd3  33460  dpmul  33461  dpmul4  33462  xrsclat  33554  nn0archi  33890  zringfrac  34068  cos9thpiminplylem4  34399  cos9thpiminplylem5  34400  cos9thpinconstr  34405  lmatfvlem  34429  xrge0iifmhm  34553  qqh0  34598  qqh1  34599  rerrext  34623  cnrrext  34624  prsiga  34745  oms0  34912  coinfliprv  35098  ballotlem1  35102  ballotth  35153  signsw0g  35168  hgt750lemd  35260  hgt750lem  35263  hgt750lem2  35264  hgt750leme  35270  tgoldbachgt  35275  subfacval2  35921  erdszelem2  35926  cvmliftlem4  36022  satom  36090  satfv1  36097  sat1el2xp  36113  fmlaomn0  36124  satfdmfmla  36134  satfv1fvfmla1  36157  ex-sategoelelomsuc  36160  ex-sategoelel12  36161  prv0  36164  prv1n  36165  elmrsubrn  36254  msubfval  36258  problem4  36402  quad3  36404  br6  36491  dfon2lem3  36517  fullfunfnv  36680  itgeq12i  36965  fneref  37108  filnetlem2  37137  filnetlem3  37138  onpsstopbas  37188  dfttc3gw  37281  dfttc4lem2  37287  dnizeq0  37311  dnibndlem12  37325  knoppcnlem5  37333  knoppcnlem8  37336  knoppcnlem11  37339  knoppndvlem14  37361  cnndvlem1  37373  bj-genr  37447  bj-genl  37448  bj-genan  37449  bj-2upln1upl  37907  bj-vtoclgfALT  37942  bj-brab2a1  38038  bj-opabssvv  38039  taupilem1  38210  qdiff  38216  topdifinf  38240  sin2h  38501  cos2h  38502  tan2h  38503  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem11  38517  poimirlem12  38518  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem22  38528  poimirlem23  38529  poimirlem24  38530  poimirlem25  38531  poimirlem26  38532  poimirlem29  38535  poimirlem31  38537  mblfinlem3  38545  mblfinlem4  38546  ismblfin  38547  itg2addnclem2  38558  asindmre  38589  heiborlem7  38719  riscer  38890  refrelcoss3  39453  symrelcoss3  39455  ishlatiN  40380  0psubN  40774  atpsubN  40778  gcdcomnni  43006  gcdnegnni  43007  neggcdnni  43008  60gcd7e1  43023  lcmeprodgcdi  43025  lcm2un  43032  lcm3un  43033  lcmineqlem4  43050  lcmineqlem6  43052  3lexlogpow5ineq1  43072  aks4d1p1p2  43088  25or6to4  43224  mzpclall  43691  diophin  43736  diophun  43737  eldioph4b  43771  irrapx1  43788  2nn0ind  43905  aomclem4  44017  onexlimgt  44203  nnoeomeqom  44272  oaomoencom  44277  oenassex  44278  succlg  44288  dflim5  44289  omabs2  44292  tfsconcatfv2  44300  ifpid3g  44451  ifpid2g  44452  ifpbi1b  44462  eu0  44479  pwinfi  44523  rtrclex  44576  cnvrcl0  44584  dfrcl2  44633  relexp1idm  44673  relexp0idm  44674  clsk1independent  45005  lhe4.4ex1a  45272  expgrowth  45278  ax6e2nd  45500  uun0.1  45719  relopabVD  45842  ax6e2ndVD  45849  sb5ALTVD  45854  ax6e2ndALT  45871  permaxinf2lem  45954  rexanuz2nf  46446  dvmptconst  46869  dvmptidg  46871  dvmulcncf  46879  dvdivcncf  46881  dvnprodlem3  46902  itgsinexplem1  46908  volioof  46941  stoweidlem13  46967  stoweidlem14  46968  stoweidlem26  46980  stoweidlem34  46988  stoweidlem49  47003  stoweidlem59  47013  dirkertrigeqlem3  47054  dirkercncflem1  47057  dirkercncflem2  47058  fourierdlem57  47117  fourierdlem62  47122  fourierdlem103  47163  fourierdlem111  47171  fourierswlem  47184  fouriersw  47185  salexct2  47293  salexct3  47296  salgencntex  47297  salgensscntex  47298  gsumge0cl  47325  sge00  47330  sge0tsms  47334  0ome  47483  ovnlecvr  47512  ovn0lem  47519  hoidmvle  47554  ovnsubadd2lem  47599  smflimlem6  47730  mbfpsssmf  47737  smfmullem4  47748  smfpimbor1lem1  47752  sqrtnzqaa  47858  numtowerdt  47860  goldratmolem2  47877  sqrtnpoly  47887  astbstanbst  47923  aistbistaandb  47924  abnotataxb  47930  aifftbifffaibif  47935  confun4  47956  plcofph  47958  plvcofph  47960  plvcofphax  47961  plvofpos  47962  mdandyv0  47963  mdandyv1  47964  mdandyv2  47965  mdandyv3  47966  mdandyv4  47967  mdandyv5  47968  mdandyv6  47969  mdandyv7  47970  mdandyv8  47971  mdandyv9  47972  mdandyv10  47973  mdandyv11  47974  mdandyv12  47975  mdandyv13  47976  mdandyv14  47977  mdandyv15  47978  mdandyvr0  47979  mdandyvr1  47980  mdandyvr2  47981  mdandyvr3  47982  mdandyvr4  47983  mdandyvr5  47984  mdandyvr6  47985  mdandyvr7  47986  mdandyvrx0  47995  mdandyvrx1  47996  mdandyvrx2  47997  mdandyvrx3  47998  mdandyvrx4  47999  mdandyvrx5  48000  mdandyvrx6  48001  mdandyvrx7  48002  dandysum2p2e4  48012  or2expropbilem1  48046  dfnelbr2  48287  2ltceilhalf  48346  flmrecm1  48357  ich2exprop  48497  paireqne  48537  fmtno4prmfac  48601  31prm  48626  lighneallem4a  48637  41prothprmlem2  48647  ppivalnn4  48656  zofldiv2ALTV  48704  nfermltl8rev  48784  nfermltl2rev  48785  nfermltlrev  48786  gbegt5  48803  gbowgt5  48804  gboge9  48806  9gbo  48816  11gbo  48817  nnsum3primes4  48830  nnsum3primesgbe  48834  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  tgblthelfgott  48857  tgoldbach  48859  ushggricedg  48969  isubgrgrim  48971  stgrvtx  48996  stgriedg  48997  stgrusgra  49001  stgr1  49003  uspgrlim  49034  grlimprclnbgrvtx  49041  clnbgr3stgrgrlic  49062  usgrexmpl1lem  49063  usgrexmpl2lem  49068  usgrexmpl2nb0  49073  usgrexmpl2nb1  49074  usgrexmpl2nb2  49075  usgrexmpl2nb3  49076  usgrexmpl2nb4  49077  usgrexmpl2nb5  49078  gpgvtx  49085  gpgiedg  49086  gpgorder  49101  gpgvtxedg0  49105  gpgvtxedg1  49106  gpgedgiov  49107  gpg5nbgrvtx03starlem1  49110  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx03starlem3  49112  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem2  49114  gpg5nbgrvtx13starlem3  49115  gpg3kgrtriexlem3  49127  gpg3kgrtriexlem6  49130  gpgprismgr4cycllem2  49138  gpgprismgr4cyclex  49149  pgnioedg1  49150  pgnioedg2  49151  pgnioedg3  49152  pgnioedg4  49153  pgnioedg5  49154  pgnbgreunbgrlem2lem1  49156  pgnbgreunbgrlem2lem2  49157  pgnbgreunbgrlem2lem3  49158  pgnbgreunbgrlem3  49160  pgnbgreunbgrlem4  49161  pgnbgreunbgrlem5lem1  49162  pgnbgreunbgrlem5lem2  49163  pgnbgreunbgrlem5lem3  49164  pgnbgreunbgrlem6  49166  gpg5ngric  49170  gpg5edgnedg  49172  nn0mnd  49220  mgmplusgiopALT  49235  sgrp2sgrp  49269  2zrngaabl  49291  funcringcsetcALTV2lem8  49338  funcringcsetclem8ALTV  49361  zlmodzxzlmod  49410  zlmodzxzel  49411  zlmodzxzscm  49413  zlmodzxzadd  49414  snlindsntorlem  49526  ldepspr  49529  lmod1lem2  49544  lmod1lem3  49545  lmod1lem4  49546  lmod1lem5  49547  lmodn0  49551  zlmodzxznm  49553  zlmodzxzldeplem  49554  zlmodzxzldeplem1  49556  zlmodzxzldeplem3  49558  lvecpsslmod  49563  ldepsnlinc  49564  ldepslinc  49565  expnegico01  49574  zofldiv2  49587  flnn0div2ge  49589  elbigo2  49608  nnlog2ge0lt1  49622  digfval  49653  dignnld  49659  dignn0flhalf  49674  2arymaptfo  49710  itcovalt2lem1  49731  prelrrx2  49769  eenglngeehlnmlem2  49794  rrxsphere  49804  line2  49808  line2x  49810  line2y  49811  itsclc0yqsollem2  49819  inlinecirc02plem  49842  sepfsepc  49980  invfn  50082  alimp-surprise  50820  aacllem  50883