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  4147  ssini  4195  opthhausdorff  5505  elvv  5741  elopaelxp  5756  relopabiv  5812  relopabi  5814  dfpo2  6304  funpr  6599  funcnvpr  6605  mpov  7535  caovcom  7620  snnex  7766  pwnex  7767  1st2val  8023  2nd2val  8024  elxp7  8030  opreuopreu  8040  poxp2  8148  poseq  8163  tfr1a  8390  oeoa  8592  oeoe  8594  erov  8821  endisj  9062  snopfsupp  9361  ssttrcl  9694  ttrclselem2  9705  r1funlim  9748  dfac2b  10133  cflecard  10254  canth4  10650  canthnumlem  10651  canthwelem  10653  canthp1lem2  10656  pwfseqlem4  10665  wunex3  10744  addsrpr  11078  mulsrpr  11079  recexsrlem  11106  mulcani  11871  div1  11922  recdiv  11939  divdiv1  11944  divdiv2  11945  div23i  11991  div11i  11992  divmuldivi  11993  divadddivi  11995  divdivdivi  11996  lemulge11  12095  negiso  12213  dfnn3  12265  2cnne0  12471  2rene0  12472  halfpm6th  12484  avglt1  12500  avglt2  12501  div4p1lem1div2  12517  3halfnz  12693  divlt1lt  13105  divle1le  13106  nnledivrp  13148  x2times  13343  xrsupsslem  13351  xrinfmsslem  13352  nnge2recico01  13552  fvf1tp  13842  om2uzoi  14011  fzennn  14024  expge1  14155  sqoddm1div8  14299  faclbnd2  14347  faclbnd4lem1  14349  4bc2eq6  14385  hashfxnn0  14393  hashsnlei  14475  hashunlei  14482  hashsslei  14483  hash2prb  14529  repswccat  14849  funcnvs4  14978  f1oun2prg  14980  wrdlen2i  15005  s2rn  15026  s3rn  15027  s7rn  15028  relexpaddg  15116  cjreb  15200  sqrt2gt1lt2  15351  abs1m  15413  bpoly3  16137  ege2le3  16169  efi4p  16218  efival  16233  sin01bnd  16266  cos01bnd  16267  cos1bnd  16268  cos2bnd  16269  sin01gt0  16271  cos01gt0  16272  sin02gt0  16273  sincos2sgn  16275  sin4lt0  16276  egt2lt3  16287  rpnnen2lem3  16297  rpnnen2lem11  16305  nthruc  16333  nthruz  16334  3dvdsdec  16415  3dvds2dec  16416  mod2eq1n2dvds  16430  halfleoddlt  16445  divalglem5  16480  ndvdsi  16495  flodddiv4  16498  flodddiv4lt  16500  bitsp1o  16516  3lcm2e6woprm  16698  6lcm4e12  16699  pcrec  16943  prmrec  17007  prmgaplcmlem1  17136  prmgaplcm  17145  modsubi  17157  structfn  17241  strleun  17242  slotsdifipndx  17413  slotsdifplendx  17453  slotsdifdsndx  17472  slotsdifunifndx  17479  slotsdifplendx2  17494  slotsdifocndx  17495  isofn  17857  sscres  17905  funcestrcsetclem7  18227  funcestrcsetclem8  18228  fullestrcsetc  18232  nulchn  18700  chninf  18716  mgmnsgrpex  19024  pwmnd  19030  ga0  19399  symg2bas  19494  f1otrspeq  19548  psgnsn  19621  0frgp  19880  gsummptnn0fz  20087  srgbinomlem4  20342  isrnghm  20556  rnghmsscmap2  20765  rnghmsscmap  20766  funcrngcsetc  20776  funcrngcsetcALT  20777  rhmsscmap2  20794  rhmsscmap  20795  funcringcsetc  20810  cnfldfun  21573  cnfldfunALT  21574  cnfld1  21584  cnsubdrglem  21605  expmhm  21623  expghm  21662  pzriprnglem4  21671  pzriprnglem9  21676  pzriprnglem14  21681  pzriprng1ALT  21683  psrbag0  22250  psrbagsn  22251  coe1fsupp  22411  coe1mul2  22467  evls1sca  22520  matmulr  22632  mat1dimelbas  22665  mat1f1o  22672  m2detleib  22825  smadiadetglem1  22865  pmatcollpw3fi1lem2  22981  cpmidpmatlem2  23065  cpmadumatpolylem1  23075  cayhamlem3  23081  cayhamlem4  23082  isbasis3g  23143  fctop  23198  cctop  23200  refref  23707  bl2in  24594  dscmet  24766  iihalf1  25127  iihalf2  25129  icopnfhmeo  25139  iccpnfhmeo  25141  xrhmeo  25142  iscvsi  25325  zclmncvs  25344  ncvs1  25353  ehl2eudis  25618  minveclem2  25622  minveclem4  25628  ovolunlem1a  25692  volf  25725  i1f1lem  25885  mbfi1fseqlem5  25915  dveflem  26175  pilem2  26652  pilem3  26653  sinhalfpilem  26665  sincosq1lem  26699  tangtx  26707  sinq12gt0  26709  sincos4thpi  26715  sincos6thpi  26718  sincos3rdpi  26719  pigt3  26720  pige3ALT  26722  coseq1  26727  efeq1  26730  efif1olem4  26747  angneg  27005  ang180lem1  27011  1cubrlem  27043  quart1  27058  log2cnv  27146  log2tlbnd  27147  log2ublem1  27148  log2ub  27151  emcllem1  27197  emcllem6  27202  basellem1  27282  basellem2  27283  basellem3  27284  basellem8  27289  ppiublem1  27403  ppiublem2  27404  ppiub  27405  chtublem  27412  chtub  27413  bcmono  27478  bclbnd  27481  bpos1lem  27483  bposlem1  27485  bposlem2  27486  bposlem3  27487  bposlem4  27488  bposlem5  27489  bposlem6  27490  bposlem7  27491  bposlem8  27492  bposlem9  27493  lgsdir2lem1  27526  1lgs  27541  gausslemma2dlem0c  27559  gausslemma2dlem0d  27560  gausslemma2dlem1a  27566  gausslemma2dlem2  27568  gausslemma2dlem3  27569  gausslemma2dlem5  27572  gausslemma2dlem6  27573  lgsquad2lem2  27586  2lgslem1a1  27590  2lgslem1a2  27591  2lgslem1c  27594  2lgslem3a  27597  2lgslem3b  27598  2lgslem3c  27599  2lgslem3d  27600  2lgslem3  27605  2lgsoddprmlem1  27609  addsqrexnreu  27643  addsqnreup  27644  chebbnd1lem1  27670  chebbnd1lem3  27672  chebbnd1  27673  dchrisum0flblem2  27710  dchrisum0lem1  27717  mulog2sumlem2  27736  selberglem2  27747  chpdifbndlem1  27754  sltssnb  27999  mulscl  28364  ltmuls  28366  divs1  28434  precsexlem8  28444  0reno  28726  1reno  28727  slotsinbpsd  28747  slotslnbpsd  28748  ercgrg  28823  axlowdimlem4  29332  axlowdimlem5  29333  axlowdimlem6  29334  axlowdimlem7  29335  axlowdimlem8  29336  axlowdimlem10  29338  axlowdimlem11  29339  graop  29416  grastruct  29417  uhgrunop  29462  upgrop  29481  upgrunop  29506  umgrunop  29508  usgrop  29550  usgr2v1e2w  29639  usgrexmpldifpr  29645  usgrexmpledg  29649  uhgrsubgrself  29667  uhgrspan1lem1  29687  upgrres1lem1  29696  fusgrfis  29717  vtxd0nedgb  29875  p1evtxdeqlem  29899  p1evtxdeq  29900  p1evtxdp1  29901  umgr2v2e  29912  vdegp1bi  29924  wlkcomp  30017  upgr2pthnlp  30118  usgr2trlncl  30146  usgr2pthlem  30149  clwlkcomp  30165  uspgrn2crct  30194  wwlksonvtx  30241  wspthnonp  30245  2wlkond  30323  2pthond  30328  2pthon3v  30329  umgr2adedgwlkonALT  30333  umgr2wlk  30335  umgr2wlkon  30336  wpthswwlks2on  30350  elwspths2spth  30356  0ewlk  30502  0pth  30513  0pthonv  30517  1pthon2v  30541  3wlkdlem4  30550  3trlond  30561  3pthond  30563  3spthond  30565  trlsegvdeglem3  30610  eupthvdres  30623  eupth2lemb  30625  ex-natded5.2i  30794  ex-an  30810  ex-id  30822  ex-po  30823  ex-fl  30835  ex-mod  30837  ex-exp  30838  ex-lcm  30846  nvz0  31057  ipidsq  31099  ipdirilem  31218  siilem1  31240  minvecolem2  31264  minvecolem3  31265  minvecolem4  31269  hvsubcan  31463  hvsubcan2  31464  normlem7tALT  31508  helch  31632  hsn0elch  31637  hhshsslem2  31657  hhsssh  31658  shscli  31706  shintcli  31718  shintcl  31719  chintcli  31720  chintcl  31721  shincli  31751  shsval2i  31776  omlsi  31793  chincli  31849  chabs1  31905  fh1i  32010  fh2i  32011  cm2ji  32014  pjnormi  32110  nmopsetn0  32254  nmfnsetn0  32267  lnophm  32408  nmcexi  32415  nmbdfnlb  32439  imaelshi  32447  nlelshi  32449  nmopadjlem  32478  nmopcoadji  32490  hmopidmch  32542  hmopidmpj  32543  sto1i  32625  stlei  32629  stji1i  32631  csmdsymi  32723  chirred  32784  cdj3lem1  32823  rpdp2cl  33238  dp2lt10  33240  dp2lt  33241  dp2ltc  33243  dpfrac1  33248  dplti  33261  dpgti  33262  dpexpp1  33264  dpadd3  33268  dpmul  33269  dpmul4  33270  xrsclat  33362  nn0archi  33698  zringfrac  33875  cos9thpiminplylem4  34206  cos9thpiminplylem5  34207  cos9thpinconstr  34212  lmatfvlem  34236  xrge0iifmhm  34360  qqh0  34405  qqh1  34406  rerrext  34430  cnrrext  34431  prsiga  34552  oms0  34719  coinfliprv  34905  ballotlem1  34909  ballotth  34960  signsw0g  34975  hgt750lemd  35067  hgt750lem  35070  hgt750lem2  35071  hgt750leme  35077  tgoldbachgt  35082  subfacval2  35700  erdszelem2  35705  cvmliftlem4  35801  satom  35869  satfv1  35876  sat1el2xp  35892  fmlaomn0  35903  satfdmfmla  35913  satfv1fvfmla1  35936  ex-sategoelelomsuc  35939  ex-sategoelel12  35940  prv0  35943  prv1n  35944  elmrsubrn  36033  msubfval  36037  problem4  36181  quad3  36183  br6  36270  dfon2lem3  36296  fullfunfnv  36459  itgeq12i  36759  fneref  36902  filnetlem2  36931  filnetlem3  36932  onpsstopbas  36982  dfttc3gw  37075  dfttc4lem2  37081  dnizeq0  37105  dnibndlem12  37119  knoppcnlem5  37127  knoppcnlem8  37130  knoppcnlem11  37133  knoppndvlem14  37155  cnndvlem1  37167  bj-genr  37241  bj-genl  37242  bj-genan  37243  bj-2upln1upl  37701  bj-vtoclgfALT  37736  bj-brab2a1  37834  bj-opabssvv  37835  taupilem1  38006  qdiff  38012  topdifinf  38036  sin2h  38302  cos2h  38303  tan2h  38304  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem11  38323  poimirlem12  38324  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem22  38334  poimirlem23  38335  poimirlem24  38336  poimirlem25  38337  poimirlem26  38338  poimirlem29  38341  poimirlem31  38343  mblfinlem3  38351  mblfinlem4  38352  ismblfin  38353  itg2addnclem2  38364  asindmre  38395  heiborlem7  38509  riscer  38680  refrelcoss3  39243  symrelcoss3  39245  ishlatiN  40170  0psubN  40564  atpsubN  40568  gcdcomnni  42796  gcdnegnni  42797  neggcdnni  42798  60gcd7e1  42813  lcmeprodgcdi  42815  lcm2un  42822  lcm3un  42823  lcmineqlem4  42840  lcmineqlem6  42842  3lexlogpow5ineq1  42862  aks4d1p1p2  42878  25or6to4  43014  mzpclall  43499  diophin  43544  diophun  43545  eldioph4b  43579  irrapx1  43596  2nn0ind  43713  aomclem4  43825  onexlimgt  44011  nnoeomeqom  44080  oaomoencom  44085  oenassex  44086  succlg  44096  dflim5  44097  omabs2  44100  tfsconcatfv2  44108  ifpid3g  44259  ifpid2g  44260  ifpbi1b  44270  eu0  44287  pwinfi  44331  rtrclex  44384  cnvrcl0  44392  dfrcl2  44441  relexp1idm  44481  relexp0idm  44482  clsk1independent  44813  lhe4.4ex1a  45080  expgrowth  45086  ax6e2nd  45308  uun0.1  45527  relopabVD  45650  ax6e2ndVD  45657  sb5ALTVD  45662  ax6e2ndALT  45679  permaxinf2lem  45762  rexanuz2nf  46247  dvmptconst  46670  dvmptidg  46672  dvmulcncf  46680  dvdivcncf  46682  dvnprodlem3  46703  itgsinexplem1  46709  volioof  46742  stoweidlem13  46768  stoweidlem14  46769  stoweidlem26  46781  stoweidlem34  46789  stoweidlem49  46804  stoweidlem59  46814  dirkertrigeqlem3  46855  dirkercncflem1  46858  dirkercncflem2  46859  fourierdlem57  46918  fourierdlem62  46923  fourierdlem103  46964  fourierdlem111  46972  fourierswlem  46985  fouriersw  46986  salexct2  47094  salexct3  47097  salgencntex  47098  salgensscntex  47099  gsumge0cl  47126  sge00  47131  sge0tsms  47135  0ome  47284  ovnlecvr  47313  ovn0lem  47320  hoidmvle  47355  ovnsubadd2lem  47400  smflimlem6  47531  mbfpsssmf  47538  smfmullem4  47549  smfpimbor1lem1  47553  sqrtnzqaa  47646  nthrucw  47648  goldratmolem2  47664  cjnpoly  47667  sinnpoly  47669  astbstanbst  47687  aistbistaandb  47688  abnotataxb  47694  aifftbifffaibif  47699  confun4  47720  plcofph  47722  plvcofph  47724  plvcofphax  47725  plvofpos  47726  mdandyv0  47727  mdandyv1  47728  mdandyv2  47729  mdandyv3  47730  mdandyv4  47731  mdandyv5  47732  mdandyv6  47733  mdandyv7  47734  mdandyv8  47735  mdandyv9  47736  mdandyv10  47737  mdandyv11  47738  mdandyv12  47739  mdandyv13  47740  mdandyv14  47741  mdandyv15  47742  mdandyvr0  47743  mdandyvr1  47744  mdandyvr2  47745  mdandyvr3  47746  mdandyvr4  47747  mdandyvr5  47748  mdandyvr6  47749  mdandyvr7  47750  mdandyvrx0  47759  mdandyvrx1  47760  mdandyvrx2  47761  mdandyvrx3  47762  mdandyvrx4  47763  mdandyvrx5  47764  mdandyvrx6  47765  mdandyvrx7  47766  dandysum2p2e4  47776  or2expropbilem1  47810  dfnelbr2  48051  2ltceilhalf  48110  flmrecm1  48121  ich2exprop  48261  paireqne  48301  fmtno4prmfac  48365  31prm  48390  lighneallem4a  48401  41prothprmlem2  48411  ppivalnn4  48420  zofldiv2ALTV  48468  nfermltl8rev  48548  nfermltl2rev  48549  nfermltlrev  48550  gbegt5  48567  gbowgt5  48568  gboge9  48570  9gbo  48580  11gbo  48581  nnsum3primes4  48594  nnsum3primesgbe  48598  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  tgblthelfgott  48621  tgoldbach  48623  ushggricedg  48733  isubgrgrim  48735  stgrvtx  48760  stgriedg  48761  stgrusgra  48765  stgr1  48767  uspgrlim  48798  grlimprclnbgrvtx  48805  clnbgr3stgrgrlic  48826  usgrexmpl1lem  48827  usgrexmpl2lem  48832  usgrexmpl2nb0  48837  usgrexmpl2nb1  48838  usgrexmpl2nb2  48839  usgrexmpl2nb3  48840  usgrexmpl2nb4  48841  usgrexmpl2nb5  48842  gpgvtx  48849  gpgiedg  48850  gpgorder  48865  gpgvtxedg0  48869  gpgvtxedg1  48870  gpgedgiov  48871  gpg5nbgrvtx03starlem1  48874  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx03starlem3  48876  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem2  48878  gpg5nbgrvtx13starlem3  48879  gpg3kgrtriexlem3  48891  gpg3kgrtriexlem6  48894  gpgprismgr4cycllem2  48902  gpgprismgr4cyclex  48913  pgnioedg1  48914  pgnioedg2  48915  pgnioedg3  48916  pgnioedg4  48917  pgnioedg5  48918  pgnbgreunbgrlem2lem1  48920  pgnbgreunbgrlem2lem2  48921  pgnbgreunbgrlem2lem3  48922  pgnbgreunbgrlem3  48924  pgnbgreunbgrlem4  48925  pgnbgreunbgrlem5lem1  48926  pgnbgreunbgrlem5lem2  48927  pgnbgreunbgrlem5lem3  48928  pgnbgreunbgrlem6  48930  gpg5ngric  48934  gpg5edgnedg  48936  nn0mnd  48985  mgmplusgiopALT  49000  sgrp2sgrp  49034  2zrngaabl  49056  funcringcsetcALTV2lem8  49103  funcringcsetclem8ALTV  49126  zlmodzxzlmod  49175  zlmodzxzel  49176  zlmodzxzscm  49178  zlmodzxzadd  49179  snlindsntorlem  49291  ldepspr  49294  lmod1lem2  49309  lmod1lem3  49310  lmod1lem4  49311  lmod1lem5  49312  lmodn0  49316  zlmodzxznm  49318  zlmodzxzldeplem  49319  zlmodzxzldeplem1  49321  zlmodzxzldeplem3  49323  lvecpsslmod  49328  ldepsnlinc  49329  ldepslinc  49330  expnegico01  49339  zofldiv2  49352  flnn0div2ge  49354  elbigo2  49373  nnlog2ge0lt1  49387  digfval  49418  dignnld  49424  dignn0flhalf  49439  2arymaptfo  49475  itcovalt2lem1  49496  prelrrx2  49534  eenglngeehlnmlem2  49559  rrxsphere  49569  line2  49573  line2x  49575  line2y  49576  itsclc0yqsollem2  49584  inlinecirc02plem  49607  sepfsepc  49747  invfn  49849  alimp-surprise  50599  aacllem  50662  2elfz13  50667