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  ssini  4139  unssi  4192  opthhausdorff  5495  elvvOLD  5732  elopaelxp  5747  relopabiv  5804  relopabi  5806  relopabiOLD  5807  dfpo2  6320  funpr  6621  funcnvpr  6627  mpov  7558  caovcom  7645  snnex  7799  pwnex  7800  1st2val  8056  2nd2val  8057  elxp7  8063  opreuopreu  8073  poxp2  8190  poseq  8205  tfr1a  8433  oeoa  8637  oeoe  8639  erov  8866  endisj  9114  snopfsupp  9413  ssttrcl  9746  ttrclselem2  9757  r1funlimOLD  9800  dfac2b  10239  cflecard  10360  canth4  10762  canthnumlem  10763  canthwelem  10765  canthp1lem2  10768  pwfseqlem4  10777  wunex3  10856  addsrpr  11190  mulsrpr  11191  recexsrlem  11218  mulcani  11985  div1  12036  recdiv  12053  divdiv1  12058  divdiv2  12059  div23i  12105  div11i  12106  divmuldivi  12107  divadddivi  12109  divdivdivi  12110  lemulge11  12209  negiso  12327  dfnn3  12379  2cnne0  12585  2rene0  12586  halfpm6th  12598  avglt1  12614  avglt2  12615  div4p1lem1div2  12631  3halfnz  12808  divlt1lt  13221  divle1le  13222  nnledivrp  13264  x2times  13459  xrsupsslem  13467  xrinfmsslem  13468  nnge2recico01  13668  fvf1tp  13959  om2uzoi  14128  fzennn  14141  expge1  14272  sqoddm1div8  14417  faclbnd2  14465  faclbnd4lem1  14467  4bc2eq6  14503  hashfxnn0  14511  hashsnlei  14593  hashunlei  14600  hashsslei  14601  hash2prb  14647  repswccat  14968  funcnvs4  15098  f1oun2prg  15100  wrdlen2i  15125  s2rn  15148  s3rn  15149  s7rn  15150  relexpaddg  15238  cjreb  15322  sqrt2gt1lt2  15473  abs1m  15535  bpoly3  16256  ege2le3  16288  efi4p  16337  efival  16352  sin01bnd  16385  cos01bnd  16386  cos1bnd  16387  cos2bnd  16388  sin01gt0  16390  cos01gt0  16391  sin02gt0  16392  sincos2sgn  16394  sin4lt0  16395  egt2lt3  16406  rpnnen2lem3  16416  rpnnen2lem11  16424  nthruc  16452  nthruz  16453  3dvdsdec  16534  3dvds2dec  16535  mod2eq1n2dvds  16549  halfleoddlt  16564  divalglem5  16599  ndvdsi  16614  flodddiv4  16617  flodddiv4lt  16619  bitsp1o  16635  3lcm2e6woprm  16822  6lcm4e12  16823  pcrec  17068  prmrec  17132  prmgaplcmlem1  17261  prmgaplcm  17270  modsubi  17282  structfn  17366  strleun  17367  slotsdifipndx  17538  slotsdifplendx  17578  slotsdifdsndx  17597  slotsdifunifndx  17604  slotsdifplendx2  17619  slotsdifocndx  17620  isofn  17982  sscres  18030  funcestrcsetclem7  18352  funcestrcsetclem8  18353  fullestrcsetc  18357  nulchn  18825  chninf  18841  mgmnsgrpex  19162  degenmgm  19169  degenmgm2nfun  19171  degenmgm2  19172  pwmnd  19175  ga0  19545  symg2bas  19640  f1otrspeq  19694  psgnsn  19767  0frgp  20026  gsummptnn0fz  20233  srgbinomlem4  20488  isrnghm  20704  rnghmsscmap2  20914  rnghmsscmap  20915  funcrngcsetc  20925  funcrngcsetcALT  20926  rhmsscmap2  20943  rhmsscmap  20944  funcringcsetc  20959  cnfldfun  21725  cnfldfunALT  21726  cnfld1  21736  cnsubdrglem  21757  expmhm  21775  expghm  21814  pzriprnglem4  21823  pzriprnglem9  21828  pzriprnglem14  21833  pzriprng1ALT  21835  psrbag0  22404  psrbagsn  22405  coe1fsupp  22565  coe1mul2  22621  evls1sca  22674  matmulr  22786  mat1dimelbas  22819  mat1f1o  22826  m2detleib  22979  smadiadetglem1  23019  pmatcollpw3fi1lem2  23138  cpmidpmatlem2  23222  cpmadumatpolylem1  23232  cayhamlem3  23238  cayhamlem4  23239  isbasis3g  23300  fctop  23355  cctop  23357  refref  23865  bl2in  24752  dscmet  24924  iihalf1  25285  iihalf2  25287  icopnfhmeo  25297  iccpnfhmeo  25299  xrhmeo  25300  iscvsi  25483  zclmncvs  25502  ncvs1  25511  ehl2eudis  25776  minveclem2  25780  minveclem4  25786  ovolunlem1a  25850  volf  25883  i1f1lem  26043  mbfi1fseqlem5  26073  dveflem  26332  pilem2  26812  pilem3  26813  sinhalfpilem  26825  sincosq1lem  26859  tangtx  26867  sinq12gt0  26869  sincos4thpi  26875  sincos6thpi  26877  sincos3rdpi  26878  pigt3  26879  pige3ALT  26881  coseq1  26886  efeq1  26889  efif1olem4  26906  angneg  27164  ang180lem1  27170  1cubrlem  27202  quart1  27217  log2cnv  27305  log2tlbnd  27306  log2ublem1  27307  log2ub  27310  emcllem1  27356  emcllem6  27361  basellem1  27441  basellem2  27442  basellem3  27443  basellem8  27448  ppiublem1  27562  ppiublem2  27563  ppiub  27564  chtublem  27571  chtub  27572  bcmono  27637  bclbnd  27640  bpos1lem  27642  bposlem1  27644  bposlem2  27645  bposlem3  27646  bposlem4  27647  bposlem5  27648  bposlem6  27649  bposlem7  27650  bposlem8  27651  bposlem9  27652  lgsdir2lem1  27685  1lgs  27700  gausslemma2dlem0c  27718  gausslemma2dlem0d  27719  gausslemma2dlem1a  27725  gausslemma2dlem2  27727  gausslemma2dlem3  27728  gausslemma2dlem5  27731  gausslemma2dlem6  27732  lgsquad2lem2  27745  2lgslem1a1  27749  2lgslem1a2  27750  2lgslem1c  27753  2lgslem3a  27756  2lgslem3b  27757  2lgslem3c  27758  2lgslem3d  27759  2lgslem3  27764  2lgsoddprmlem1  27768  addsqrexnreu  27802  addsqnreup  27803  chebbnd1lem1  27829  chebbnd1lem3  27831  chebbnd1  27832  dchrisum0flblem2  27869  dchrisum0lem1  27876  mulog2sumlem2  27895  selberglem2  27906  chpdifbndlem1  27913  sltssnb  28188  mulscl  28553  ltmuls  28555  divs1  28623  precsexlem8  28633  0reno  28915  1reno  28916  slotsinbpsd  28936  slotslnbpsd  28937  ercgrg  29013  axlowdimlem4  29556  axlowdimlem5  29557  axlowdimlem6  29558  axlowdimlem7  29559  axlowdimlem8  29560  axlowdimlem10  29562  axlowdimlem11  29563  graop  29640  grastruct  29641  uhgrunop  29686  upgrop  29705  upgrunop  29730  umgrunop  29732  usgrop  29777  usgr2v1e2w  29866  usgrexmpldifpr  29872  usgrexmpledg  29876  uhgrsubgrself  29894  uhgrspan1lem1  29914  upgrres1lem1  29923  fusgrfis  29944  vtxd0nedgb  30102  p1evtxdeqlem  30126  p1evtxdeq  30127  p1evtxdp1  30128  umgr2v2e  30139  vdegp1bi  30151  wlkcomp  30244  upgr2pthnlp  30351  usgr2trlncl  30379  usgr2pthlem  30382  clwlkcomp  30399  uspgrn2crct  30430  wwlksonvtx  30477  wspthnonp  30481  2wlkond  30559  2pthond  30564  2pthon3v  30565  umgr2adedgwlkonALT  30569  umgr2wlk  30571  umgr2wlkon  30572  wpthswwlks2on  30586  elwspths2spth  30592  0ewlk  30738  0pth  30749  0pthonv  30753  1pthon2v  30787  3wlkdlem4  30796  3trlond  30807  3pthond  30809  3spthond  30811  trlsegvdeglem3  30856  eupthvdres  30869  eupth2lemb  30871  ex-natded5.2i  31040  ex-an  31056  ex-id  31068  ex-po  31069  ex-fl  31081  ex-mod  31083  ex-exp  31084  ex-lcm  31092  nvz0  31303  ipidsq  31345  ipdirilem  31464  siilem1  31486  minvecolem2  31510  minvecolem3  31511  minvecolem4  31515  hvsubcan  31709  hvsubcan2  31710  normlem7tALT  31754  helch  31878  hsn0elch  31883  hhshsslem2  31903  hhsssh  31904  shscli  31952  shintcli  31964  shintcl  31965  chintcli  31966  chintcl  31967  shincli  31997  shsval2i  32022  omlsi  32039  chincli  32095  chabs1  32151  fh1i  32256  fh2i  32257  cm2ji  32260  pjnormi  32356  nmopsetn0  32500  nmfnsetn0  32513  lnophm  32654  nmcexi  32661  nmbdfnlb  32685  imaelshi  32693  nlelshi  32695  nmopadjlem  32724  nmopcoadji  32736  hmopidmch  32788  hmopidmpj  32789  sto1i  32871  stlei  32875  stji1i  32877  csmdsymi  32969  chirred  33030  cdj3lem1  33069  rpdp2cl  33521  dp2lt10  33523  dp2lt  33524  dp2ltc  33526  dpfrac1  33531  dplti  33544  dpgti  33545  dpexpp1  33547  dpadd3  33551  dpmul  33552  dpmul4  33553  xrsclat  33648  zzedom  33939  nn0archi  33992  zringfrac  34169  cos9thpiminplylem4  34500  cos9thpiminplylem5  34501  cos9thpinconstr  34506  lmatfvlem  34530  xrge0iifmhm  34654  qqh0  34699  qqh1  34700  rerrext  34724  cnrrext  34725  prsiga  34846  oms0  35012  coinfliprv  35198  ballotlem1  35202  ballotth  35253  signsw0g  35268  hgt750lemd  35360  hgt750lem  35363  hgt750lem2  35364  hgt750leme  35370  tgoldbachgt  35375  omeueq  35809  subfacval2  36132  erdszelem2  36137  cvmliftlem4  36233  satom  36301  satfv1  36308  sat1el2xp  36324  fmlaomn0  36335  satfdmfmla  36345  satfv1fvfmla1  36368  ex-sategoelelomsuc  36371  ex-sategoelel12  36372  prv0  36375  prv1n  36376  elmrsubrn  36465  msubfval  36469  problem4  36613  quad3  36615  br6  36713  dfon2lem3  36738  fullfunfnv  36901  itgeq12i  37186  fneref  37329  filnetlem2  37358  filnetlem3  37359  onpsstopbas  37409  dfttc3gw  37502  dfttc4lem2  37508  dnizeq0  37532  dnibndlem12  37546  knoppcnlem5  37554  knoppcnlem8  37557  knoppcnlem11  37560  knoppndvlem14  37582  cnndvlem1  37594  bj-genr  37668  bj-genl  37669  bj-genan  37670  bj-2upln1upl  38128  bj-vtoclgfALT  38178  bj-brab2a1  38275  bj-opabssvv  38276  taupilem1  38447  qdiff  38453  topdifinf  38477  sin2h  38738  cos2h  38739  tan2h  38740  poimirlem1  38744  poimirlem2  38745  poimirlem3  38746  poimirlem4  38747  poimirlem6  38749  poimirlem7  38750  poimirlem11  38754  poimirlem12  38755  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  poimirlem22  38765  poimirlem23  38766  poimirlem24  38767  poimirlem25  38768  poimirlem26  38769  poimirlem29  38772  poimirlem31  38774  mblfinlem3  38782  mblfinlem4  38783  ismblfin  38784  itg2addnclem2  38795  asindmre  38826  heiborlem7  38954  riscer  39125  refrelcoss3  39688  symrelcoss3  39690  ishlatiN  40615  0psubN  41009  atpsubN  41013  gcdcomnni  43241  gcdnegnni  43242  neggcdnni  43243  60gcd7e1  43258  lcmeprodgcdi  43260  lcm2un  43267  lcm3un  43268  lcmineqlem4  43285  lcmineqlem6  43287  3lexlogpow5ineq1  43307  aks4d1p1p2  43323  25or6to4  43459  mzpclall  43942  diophin  43987  diophun  43988  eldioph4b  44022  irrapx1  44039  2nn0ind  44156  aomclem4  44263  onexlimgt  44448  nnoeomeqom  44517  oaomoencom  44522  oenassex  44523  succlg  44533  dflim5  44534  omabs2  44537  tfsconcatfv2  44545  ifpid3g  44696  ifpid2g  44697  ifpbi1b  44707  eu0  44724  pwinfi  44768  rtrclex  44820  cnvrcl0  44828  dfrcl2  44877  relexp1idm  44917  relexp0idm  44918  clsk1independent  45249  lhe4.4ex1a  45516  expgrowth  45522  ax6e2nd  45743  uun0.1  45962  relopabVD  46085  ax6e2ndVD  46092  sb5ALTVD  46097  ax6e2ndALT  46114  permaxinf2lem  46208  rexanuz2nf  46717  dvmptconst  47140  dvmptidg  47142  dvmulcncf  47150  dvdivcncf  47152  dvnprodlem3  47173  itgsinexplem1  47179  volioof  47212  stoweidlem13  47238  stoweidlem14  47239  stoweidlem26  47251  stoweidlem34  47259  stoweidlem49  47274  stoweidlem59  47284  dirkertrigeqlem3  47325  dirkercncflem1  47328  dirkercncflem2  47329  fourierdlem57  47388  fourierdlem62  47393  fourierdlem103  47434  fourierdlem111  47442  fourierswlem  47455  fouriersw  47456  salexct2  47564  salexct3  47567  salgencntex  47568  salgensscntex  47569  gsumge0cl  47596  sge00  47601  sge0tsms  47605  0ome  47754  ovnlecvr  47783  ovn0lem  47790  hoidmvle  47825  ovnsubadd2lem  47870  smflimlem6  48001  mbfpsssmf  48008  smfmullem4  48019  smfpimbor1lem1  48023  sqrtnzqaa  48129  numtowerdt  48131  goldratmolem2  48148  sqrtnpoly  48158  astbstanbst  48194  aistbistaandb  48195  abnotataxb  48201  aifftbifffaibif  48206  confun4  48227  plcofph  48229  plvcofph  48231  plvcofphax  48232  plvofpos  48233  mdandyv0  48234  mdandyv1  48235  mdandyv2  48236  mdandyv3  48237  mdandyv4  48238  mdandyv5  48239  mdandyv6  48240  mdandyv7  48241  mdandyv8  48242  mdandyv9  48243  mdandyv10  48244  mdandyv11  48245  mdandyv12  48246  mdandyv13  48247  mdandyv14  48248  mdandyv15  48249  mdandyvr0  48250  mdandyvr1  48251  mdandyvr2  48252  mdandyvr3  48253  mdandyvr4  48254  mdandyvr5  48255  mdandyvr6  48256  mdandyvr7  48257  mdandyvrx0  48266  mdandyvrx1  48267  mdandyvrx2  48268  mdandyvrx3  48269  mdandyvrx4  48270  mdandyvrx5  48271  mdandyvrx6  48272  mdandyvrx7  48273  dandysum2p2e4  48283  or2expropbilem1  48317  dfnelbr2  48558  2ltceilhalf  48617  flmrecm1  48628  ich2exprop  48768  paireqne  48808  fmtno4prmfac  48872  31prm  48897  lighneallem4a  48908  41prothprmlem2  48918  ppivalnn4  48927  zofldiv2ALTV  48975  nfermltl8rev  49055  nfermltl2rev  49056  nfermltlrev  49057  gbegt5  49074  gbowgt5  49075  gboge9  49077  9gbo  49087  11gbo  49088  nnsum3primes4  49101  nnsum3primesgbe  49105  nnsum4primesodd  49109  nnsum4primesoddALTV  49110  nnsum4primeseven  49113  nnsum4primesevenALTV  49114  tgblthelfgott  49128  tgoldbach  49130  ushggricedg  49240  isubgrgrim  49242  stgrvtx  49267  stgriedg  49268  stgrusgra  49272  stgr1  49274  uspgrlim  49305  grlimprclnbgrvtx  49312  clnbgr3stgrgrlic  49333  usgrexmpl1lem  49334  usgrexmpl2lem  49339  usgrexmpl2nb0  49344  usgrexmpl2nb1  49345  usgrexmpl2nb2  49346  usgrexmpl2nb3  49347  usgrexmpl2nb4  49348  usgrexmpl2nb5  49349  gpgvtx  49356  gpgiedg  49357  gpgorder  49372  gpgvtxedg0  49376  gpgvtxedg1  49377  gpgedgiov  49378  gpg5nbgrvtx03starlem1  49381  gpg5nbgrvtx03starlem2  49382  gpg5nbgrvtx03starlem3  49383  gpg5nbgrvtx13starlem1  49384  gpg5nbgrvtx13starlem2  49385  gpg5nbgrvtx13starlem3  49386  gpg3kgrtriexlem3  49398  gpg3kgrtriexlem6  49401  gpgprismgr4cycllem2  49409  gpgprismgr4cyclex  49420  pgnioedg1  49421  pgnioedg2  49422  pgnioedg3  49423  pgnioedg4  49424  pgnioedg5  49425  pgnbgreunbgrlem2lem1  49427  pgnbgreunbgrlem2lem2  49428  pgnbgreunbgrlem2lem3  49429  pgnbgreunbgrlem3  49431  pgnbgreunbgrlem4  49432  pgnbgreunbgrlem5lem1  49433  pgnbgreunbgrlem5lem2  49434  pgnbgreunbgrlem5lem3  49435  pgnbgreunbgrlem6  49437  gpg5ngric  49441  gpg5edgnedg  49443  nn0mnd  49491  mgmplusgiopALT  49506  sgrp2sgrp  49540  2zrngaabl  49562  funcringcsetcALTV2lem8  49609  funcringcsetclem8ALTV  49632  zlmodzxzlmod  49681  zlmodzxzel  49682  zlmodzxzscm  49684  zlmodzxzadd  49685  snlindsntorlem  49797  ldepspr  49800  lmod1lem2  49815  lmod1lem3  49816  lmod1lem4  49817  lmod1lem5  49818  lmodn0  49822  zlmodzxznm  49824  zlmodzxzldeplem  49825  zlmodzxzldeplem1  49827  zlmodzxzldeplem3  49829  lvecpsslmod  49834  ldepsnlinc  49835  ldepslinc  49836  expnegico01  49845  zofldiv2  49858  flnn0div2ge  49860  elbigo2  49879  nnlog2ge0lt1  49893  digfval  49924  dignnld  49930  dignn0flhalf  49945  2arymaptfo  49981  itcovalt2lem1  50002  eenglngeehlnmlem2  50066  rrxsphere  50075  line2  50079  line2x  50081  line2y  50082  itsclc0yqsollem2  50090  sepfsepc  50257  invfn  50359  par2hom  50994  fuconuniqvalslem  50998  sinhadd  51138  alimp-surprise  51188  aacllem  51251