Theorem pm3.2i 474

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

Syntax hints:   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mp4an  703  pm4.87  854  3pm3.2i  1352  sbt  2094  unssi  4143  ssini  4191  opthhausdorff  5485  elvv  5720  elopaelxp  5735  relopabiv  5791  relopabi  5793  dfpo2  6279  funpr  6573  funcnvpr  6579  mpov  7504  caovcom  7589  snnex  7737  pwnex  7738  1st2val  7994  2nd2val  7995  elxp7  8001  opreuopreu  8011  poxp2  8118  poseq  8133  tfr1a  8360  oeoa  8562  oeoe  8564  erov  8791  endisj  9032  snopfsupp  9334  ssttrcl  9667  ttrclselem2  9678  r1funlim  9721  dfac2b  10084  cflecard  10206  canth4  10602  canthnumlem  10603  canthwelem  10605  canthp1lem2  10608  pwfseqlem4  10617  wunex3  10696  addsrpr  11030  mulsrpr  11031  recexsrlem  11058  mulcani  11823  div1  11877  recdiv  11894  divdiv1  11899  divdiv2  11900  div23i  11946  div11i  11947  divmuldivi  11948  divadddivi  11950  divdivdivi  11951  lemulge11  12051  negiso  12169  dfnn3  12221  2cnne0  12427  2rene0  12428  halfpm6th  12440  avglt1  12456  avglt2  12457  div4p1lem1div2  12473  3halfnz  12649  divlt1lt  13061  divle1le  13062  nnledivrp  13104  x2times  13299  xrsupsslem  13307  xrinfmsslem  13308  nnge2recico01  13508  fvf1tp  13796  om2uzoi  13965  fzennn  13978  expge1  14109  sqoddm1div8  14253  faclbnd2  14301  faclbnd4lem1  14303  4bc2eq6  14339  hashfxnn0  14347  hashsnlei  14428  hashunlei  14435  hashsslei  14436  hash2prb  14482  repswccat  14796  funcnvs4  14925  f1oun2prg  14927  wrdlen2i  14952  s2rn  14973  s3rn  14974  s7rn  14975  relexpaddg  15063  cjreb  15133  sqrt2gt1lt2  15284  abs1m  15346  bpoly3  16071  ege2le3  16103  efi4p  16152  efival  16167  sin01bnd  16200  cos01bnd  16201  cos1bnd  16202  cos2bnd  16203  sin01gt0  16205  cos01gt0  16206  sin02gt0  16207  sincos2sgn  16209  sin4lt0  16210  egt2lt3  16221  rpnnen2lem3  16231  rpnnen2lem11  16239  nthruc  16267  nthruz  16268  3dvdsdec  16349  3dvds2dec  16350  mod2eq1n2dvds  16364  halfleoddlt  16379  divalglem5  16414  ndvdsi  16429  flodddiv4  16432  flodddiv4lt  16434  bitsp1o  16450  3lcm2e6woprm  16632  6lcm4e12  16633  pcrec  16877  prmrec  16941  prmgaplcmlem1  17070  prmgaplcm  17079  modsubi  17091  structfn  17175  strleun  17176  slotsdifipndx  17347  slotsdifplendx  17387  slotsdifdsndx  17406  slotsdifunifndx  17413  slotsdifplendx2  17428  slotsdifocndx  17429  isofn  17791  sscres  17839  funcestrcsetclem7  18161  funcestrcsetclem8  18162  fullestrcsetc  18166  nulchn  18634  chninf  18650  mgmnsgrpex  18951  pwmnd  18957  ga0  19321  symg2bas  19416  f1otrspeq  19470  psgnsn  19543  0frgp  19802  gsummptnn0fz  20009  srgbinomlem4  20258  isrnghm  20469  rnghmsscmap2  20658  rnghmsscmap  20659  funcrngcsetc  20669  funcrngcsetcALT  20670  rhmsscmap2  20687  rhmsscmap  20688  funcringcsetc  20703  cnfldfun  21418  cnfldfunALT  21419  cnfld1  21429  cnsubdrglem  21450  expmhm  21468  expghm  21507  pzriprnglem4  21516  pzriprnglem9  21521  pzriprnglem14  21526  pzriprng1ALT  21528  psrbag0  22095  psrbagsn  22096  coe1fsupp  22256  coe1mul2  22312  evls1sca  22366  matmulr  22478  mat1dimelbas  22511  mat1f1o  22518  m2detleib  22671  smadiadetglem1  22711  pmatcollpw3fi1lem2  22827  cpmidpmatlem2  22911  cpmadumatpolylem1  22921  cayhamlem3  22927  cayhamlem4  22928  isbasis3g  22989  fctop  23044  cctop  23046  refref  23553  bl2in  24440  dscmet  24612  iihalf1  24973  iihalf2  24975  icopnfhmeo  24985  iccpnfhmeo  24987  xrhmeo  24988  iscvsi  25171  zclmncvs  25190  ncvs1  25199  ehl2eudis  25464  minveclem2  25468  minveclem4  25474  ovolunlem1a  25538  volf  25571  i1f1lem  25731  mbfi1fseqlem5  25761  dveflem  26021  pilem2  26492  pilem3  26493  sinhalfpilem  26505  sincosq1lem  26539  tangtx  26547  sinq12gt0  26549  sincos4thpi  26555  sincos6thpi  26558  sincos3rdpi  26559  pigt3  26560  pige3ALT  26562  coseq1  26567  efeq1  26570  efif1olem4  26587  angneg  26845  ang180lem1  26851  1cubrlem  26883  quart1  26898  log2cnv  26986  log2tlbnd  26987  log2ublem1  26988  log2ub  26991  emcllem1  27037  emcllem6  27042  basellem1  27122  basellem2  27123  basellem3  27124  basellem8  27129  ppiublem1  27243  ppiublem2  27244  ppiub  27245  chtublem  27252  chtub  27253  bcmono  27318  bclbnd  27321  bpos1lem  27323  bposlem1  27325  bposlem2  27326  bposlem3  27327  bposlem4  27328  bposlem5  27329  bposlem6  27330  bposlem7  27331  bposlem8  27332  bposlem9  27333  lgsdir2lem1  27366  1lgs  27381  gausslemma2dlem0c  27399  gausslemma2dlem0d  27400  gausslemma2dlem1a  27406  gausslemma2dlem2  27408  gausslemma2dlem3  27409  gausslemma2dlem5  27412  gausslemma2dlem6  27413  lgsquad2lem2  27426  2lgslem1a1  27430  2lgslem1a2  27431  2lgslem1c  27434  2lgslem3a  27437  2lgslem3b  27438  2lgslem3c  27439  2lgslem3d  27440  2lgslem3  27445  2lgsoddprmlem1  27449  addsqrexnreu  27483  addsqnreup  27484  chebbnd1lem1  27510  chebbnd1lem3  27512  chebbnd1  27513  dchrisum0flblem2  27550  dchrisum0lem1  27557  mulog2sumlem2  27576  selberglem2  27587  chpdifbndlem1  27594  sltssnb  27839  mulscl  28204  ltmuls  28206  divs1  28274  precsexlem8  28284  0reno  28566  1reno  28567  slotsinbpsd  28587  slotslnbpsd  28588  ercgrg  28663  axlowdimlem4  29092  axlowdimlem5  29093  axlowdimlem6  29094  axlowdimlem7  29095  axlowdimlem8  29096  axlowdimlem10  29098  axlowdimlem11  29099  graop  29176  grastruct  29177  uhgrunop  29222  upgrop  29241  upgrunop  29266  umgrunop  29268  usgrop  29310  usgr2v1e2w  29399  usgrexmpldifpr  29405  usgrexmpledg  29409  uhgrsubgrself  29427  uhgrspan1lem1  29447  upgrres1lem1  29456  fusgrfis  29477  vtxd0nedgb  29635  p1evtxdeqlem  29659  p1evtxdeq  29660  p1evtxdp1  29661  umgr2v2e  29672  vdegp1bi  29684  wlkcomp  29777  upgr2pthnlp  29878  usgr2trlncl  29906  usgr2pthlem  29909  clwlkcomp  29925  uspgrn2crct  29954  wwlksonvtx  30001  wspthnonp  30005  2wlkond  30083  2pthond  30088  2pthon3v  30089  umgr2adedgwlkonALT  30093  umgr2wlk  30095  umgr2wlkon  30096  wpthswwlks2on  30110  elwspths2spth  30116  0ewlk  30262  0pth  30273  0pthonv  30277  1pthon2v  30301  3wlkdlem4  30310  3trlond  30321  3pthond  30323  3spthond  30325  trlsegvdeglem3  30370  eupthvdres  30383  eupth2lemb  30385  ex-natded5.2i  30554  ex-an  30570  ex-id  30582  ex-po  30583  ex-fl  30595  ex-mod  30597  ex-exp  30598  ex-lcm  30606  nvz0  30817  ipidsq  30859  ipdirilem  30978  siilem1  31000  minvecolem2  31024  minvecolem3  31025  minvecolem4  31029  hvsubcan  31223  hvsubcan2  31224  normlem7tALT  31268  helch  31392  hsn0elch  31397  hhshsslem2  31417  hhsssh  31418  shscli  31466  shintcli  31478  shintcl  31479  chintcli  31480  chintcl  31481  shincli  31511  shsval2i  31536  omlsi  31553  chincli  31609  chabs1  31665  fh1i  31770  fh2i  31771  cm2ji  31774  pjnormi  31870  nmopsetn0  32014  nmfnsetn0  32027  lnophm  32168  nmcexi  32175  nmbdfnlb  32199  imaelshi  32207  nlelshi  32209  nmopadjlem  32238  nmopcoadji  32250  hmopidmch  32302  hmopidmpj  32303  sto1i  32385  stlei  32389  stji1i  32391  csmdsymi  32483  chirred  32544  cdj3lem1  32583  rpdp2cl  33020  dp2lt10  33022  dp2lt  33023  dp2ltc  33025  dpfrac1  33030  dplti  33043  dpgti  33044  dpexpp1  33046  dpadd3  33050  dpmul  33051  dpmul4  33052  xrsclat  33150  nn0archi  33494  zringfrac  33711  cos9thpiminplylem4  34043  cos9thpiminplylem5  34044  cos9thpinconstr  34049  lmatfvlem  34073  xrge0iifmhm  34197  qqh0  34242  qqh1  34243  rerrext  34267  cnrrext  34268  prsiga  34389  oms0  34555  coinfliprv  34741  ballotlem1  34745  ballotth  34796  signsw0g  34814  hgt750lemd  34906  hgt750lem  34909  hgt750lem2  34910  hgt750leme  34916  tgoldbachgt  34921  subfacval2  35501  erdszelem2  35506  cvmliftlem4  35602  satom  35670  satfv1  35677  sat1el2xp  35693  fmlaomn0  35704  satfdmfmla  35714  satfv1fvfmla1  35737  ex-sategoelelomsuc  35740  ex-sategoelel12  35741  prv0  35744  prv1n  35745  elmrsubrn  35834  msubfval  35838  problem4  35982  quad3  35984  br6  36071  dfon2lem3  36097  fullfunfnv  36260  itgeq12i  36530  fneref  36674  filnetlem2  36703  filnetlem3  36704  onpsstopbas  36754  dfttc3gw  36847  dfttc4lem2  36853  dnizeq0  36877  dnibndlem12  36891  knoppcnlem5  36899  knoppcnlem8  36902  knoppcnlem11  36905  knoppndvlem14  36927  cnndvlem1  36939  bj-genr  37014  bj-genl  37015  bj-genan  37016  bj-2upln1upl  37473  bj-vtoclgfALT  37508  bj-brab2a1  37605  bj-opabssvv  37606  taupilem1  37777  qdiff  37783  topdifinf  37807  sin2h  38073  cos2h  38074  tan2h  38075  poimirlem1  38084  poimirlem2  38085  poimirlem3  38086  poimirlem4  38087  poimirlem6  38089  poimirlem7  38090  poimirlem11  38094  poimirlem12  38095  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem22  38105  poimirlem23  38106  poimirlem24  38107  poimirlem25  38108  poimirlem26  38109  poimirlem29  38112  poimirlem31  38114  mblfinlem3  38122  mblfinlem4  38123  ismblfin  38124  itg2addnclem2  38135  asindmre  38166  heiborlem7  38280  riscer  38451  refrelcoss3  39016  symrelcoss3  39018  ishlatiN  39943  0psubN  40337  atpsubN  40341  gcdcomnni  42569  gcdnegnni  42570  neggcdnni  42571  60gcd7e1  42586  lcmeprodgcdi  42588  lcm2un  42595  lcm3un  42596  lcmineqlem4  42613  lcmineqlem6  42615  3lexlogpow5ineq1  42635  aks4d1p1p2  42651  mzpclall  43272  diophin  43317  diophun  43318  eldioph4b  43352  irrapx1  43369  2nn0ind  43486  aomclem4  43598  onexlimgt  43784  nnoeomeqom  43853  oaomoencom  43858  oenassex  43859  succlg  43869  dflim5  43870  omabs2  43873  tfsconcatfv2  43881  ifpid3g  44032  ifpid2g  44033  ifpbi1b  44043  eu0  44060  pwinfi  44104  rtrclex  44157  cnvrcl0  44165  dfrcl2  44214  relexp1idm  44254  relexp0idm  44255  clsk1independent  44586  lhe4.4ex1a  44869  expgrowth  44875  ax6e2nd  45098  uun0.1  45317  relopabVD  45440  ax6e2ndVD  45447  sb5ALTVD  45452  ax6e2ndALT  45469  permaxinf2lem  45552  rexanuz2nf  46030  dvmptconst  46453  dvmptidg  46455  dvmulcncf  46463  dvdivcncf  46465  dvnprodlem3  46486  itgsinexplem1  46492  volioof  46525  stoweidlem13  46551  stoweidlem14  46552  stoweidlem26  46564  stoweidlem34  46572  stoweidlem49  46587  stoweidlem59  46597  dirkertrigeqlem3  46638  dirkercncflem1  46641  dirkercncflem2  46642  fourierdlem57  46701  fourierdlem62  46706  fourierdlem103  46747  fourierdlem111  46755  fourierswlem  46768  fouriersw  46769  salexct2  46877  salexct3  46880  salgencntex  46881  salgensscntex  46882  gsumge0cl  46909  sge00  46914  sge0tsms  46918  0ome  47067  ovnlecvr  47096  ovn0lem  47103  hoidmvle  47138  ovnsubadd2lem  47183  smflimlem6  47314  mbfpsssmf  47321  smfmullem4  47332  smfpimbor1lem1  47336  nthrucw  47426  goldratmolem2  47444  cjnpoly  47447  sinnpoly  47449  astbstanbst  47467  aistbistaandb  47468  abnotataxb  47474  aifftbifffaibif  47479  confun4  47500  plcofph  47502  plvcofph  47504  plvcofphax  47505  plvofpos  47506  mdandyv0  47507  mdandyv1  47508  mdandyv2  47509  mdandyv3  47510  mdandyv4  47511  mdandyv5  47512  mdandyv6  47513  mdandyv7  47514  mdandyv8  47515  mdandyv9  47516  mdandyv10  47517  mdandyv11  47518  mdandyv12  47519  mdandyv13  47520  mdandyv14  47521  mdandyv15  47522  mdandyvr0  47523  mdandyvr1  47524  mdandyvr2  47525  mdandyvr3  47526  mdandyvr4  47527  mdandyvr5  47528  mdandyvr6  47529  mdandyvr7  47530  mdandyvrx0  47539  mdandyvrx1  47540  mdandyvrx2  47541  mdandyvrx3  47542  mdandyvrx4  47543  mdandyvrx5  47544  mdandyvrx6  47545  mdandyvrx7  47546  dandysum2p2e4  47556  or2expropbilem1  47590  dfnelbr2  47831  2ltceilhalf  47890  flmrecm1  47901  ich2exprop  48041  paireqne  48081  fmtno4prmfac  48145  31prm  48170  lighneallem4a  48181  41prothprmlem2  48191  ppivalnn4  48200  zofldiv2ALTV  48248  nfermltl8rev  48328  nfermltl2rev  48329  nfermltlrev  48330  gbegt5  48347  gbowgt5  48348  gboge9  48350  9gbo  48360  11gbo  48361  nnsum3primes4  48374  nnsum3primesgbe  48378  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  tgblthelfgott  48401  tgoldbach  48403  ushggricedg  48513  isubgrgrim  48515  stgrvtx  48540  stgriedg  48541  stgrusgra  48545  stgr1  48547  uspgrlim  48578  grlimprclnbgrvtx  48585  clnbgr3stgrgrlic  48606  usgrexmpl1lem  48607  usgrexmpl2lem  48612  usgrexmpl2nb0  48617  usgrexmpl2nb1  48618  usgrexmpl2nb2  48619  usgrexmpl2nb3  48620  usgrexmpl2nb4  48621  usgrexmpl2nb5  48622  gpgvtx  48629  gpgiedg  48630  gpgorder  48645  gpgvtxedg0  48649  gpgvtxedg1  48650  gpgedgiov  48651  gpg5nbgrvtx03starlem1  48654  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx03starlem3  48656  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem2  48658  gpg5nbgrvtx13starlem3  48659  gpg3kgrtriexlem3  48671  gpg3kgrtriexlem6  48674  gpgprismgr4cycllem2  48682  gpgprismgr4cyclex  48693  pgnioedg1  48694  pgnioedg2  48695  pgnioedg3  48696  pgnioedg4  48697  pgnioedg5  48698  pgnbgreunbgrlem2lem1  48700  pgnbgreunbgrlem2lem2  48701  pgnbgreunbgrlem2lem3  48702  pgnbgreunbgrlem3  48704  pgnbgreunbgrlem4  48705  pgnbgreunbgrlem5lem1  48706  pgnbgreunbgrlem5lem2  48707  pgnbgreunbgrlem5lem3  48708  pgnbgreunbgrlem6  48710  gpg5ngric  48714  gpg5edgnedg  48716  nn0mnd  48765  mgmplusgiopALT  48780  sgrp2sgrp  48814  2zrngaabl  48836  funcringcsetcALTV2lem8  48883  funcringcsetclem8ALTV  48906  zlmodzxzlmod  48940  zlmodzxzel  48941  zlmodzxzscm  48943  zlmodzxzadd  48944  snlindsntorlem  49056  ldepspr  49059  lmod1lem2  49074  lmod1lem3  49075  lmod1lem4  49076  lmod1lem5  49077  lmodn0  49081  zlmodzxznm  49083  zlmodzxzldeplem  49084  zlmodzxzldeplem1  49086  zlmodzxzldeplem3  49088  lvecpsslmod  49093  ldepsnlinc  49094  ldepslinc  49095  expnegico01  49104  zofldiv2  49117  flnn0div2ge  49119  elbigo2  49138  nnlog2ge0lt1  49152  digfval  49183  dignnld  49189  dignn0flhalf  49204  2arymaptfo  49240  itcovalt2lem1  49261  prelrrx2  49299  eenglngeehlnmlem2  49324  rrxsphere  49334  line2  49338  line2x  49340  line2y  49341  itsclc0yqsollem2  49349  inlinecirc02plem  49372  sepfsepc  49513  invfn  49615  alimp-surprise  50365  aacllem  50386