Theorem pm3.2i 474

Description: Infer conjunction of premises. Inference associated with pm3.2 473. Its associated deduction is jca 515 (and the double deduction is jcad 516). (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 210  df-an 400

This theorem is referenced by:  mp4an  693  pm4.87  843  3pm3.2i  1341  unssi  4099  ssini  4146  opthhausdorff  5400  elvv  5623  relopabiv  5690  relopabi  5692  funpr  6436  funcnvpr  6442  mpov  7322  caovcom  7405  snnex  7543  pwnex  7544  1st2val  7789  2nd2val  7790  elxp7  7796  opreuopreu  7806  mptmpoopabbrd  7851  wfrlem13  8067  wfr3  8075  tfr1a  8130  oeoa  8325  oeoe  8327  erov  8496  endisj  8732  phplem2  8826  snopfsupp  9008  r1funlim  9382  dfac2b  9744  cflecard  9867  canth4  10261  canthnumlem  10262  canthwelem  10264  canthp1lem2  10267  pwfseqlem4  10276  wunex3  10355  addsrpr  10689  mulsrpr  10690  recexsrlem  10717  mulcani  11471  div1  11521  recdiv  11538  divdiv1  11543  divdiv2  11544  div23i  11590  div11i  11591  divmuldivi  11592  divadddivi  11594  divdivdivi  11595  lemulge11  11694  negiso  11812  dfnn3  11844  2cnne0  12040  2rene0  12041  halfpm6th  12051  avglt1  12068  avglt2  12069  div4p1lem1div2  12085  3halfnz  12256  divlt1lt  12655  divle1le  12656  nnledivrp  12698  x2times  12889  xrsupsslem  12897  xrinfmsslem  12898  fz0to4untppr  13215  om2uzoi  13528  fzennn  13541  expge1  13672  sqoddm1div8  13810  faclbnd2  13857  faclbnd4lem1  13859  4bc2eq6  13895  hashfxnn0  13903  hashsnlei  13985  hashunlei  13992  hashsslei  13993  hash2prb  14038  repswccat  14351  cshwsexa  14389  funcnvs4  14480  f1oun2prg  14482  wrdlen2i  14507  relexpaddg  14616  cjreb  14686  sqrt2gt1lt2  14838  abs1m  14899  bpoly3  15620  ege2le3  15651  efi4p  15698  efival  15713  sin01bnd  15746  cos01bnd  15747  cos1bnd  15748  cos2bnd  15749  sin01gt0  15751  cos01gt0  15752  sin02gt0  15753  sincos2sgn  15755  sin4lt0  15756  egt2lt3  15767  rpnnen2lem3  15777  rpnnen2lem11  15785  nthruc  15813  nthruz  15814  3dvdsdec  15893  3dvds2dec  15894  mod2eq1n2dvds  15908  halfleoddlt  15923  divalglem5  15958  ndvdsi  15973  flodddiv4  15974  flodddiv4lt  15976  bitsp1o  15992  3lcm2e6woprm  16172  6lcm4e12  16173  pcrec  16411  prmrec  16475  prmgaplcmlem1  16604  prmgaplcm  16613  modsubi  16625  structfn  16709  strleun  16710  isofn  17280  sscres  17328  funcestrcsetclem7  17653  funcestrcsetclem8  17654  fullestrcsetc  17658  mgmnsgrpex  18358  pwmnd  18364  ga0  18692  symg2bas  18785  f1otrspeq  18839  psgnsn  18912  0frgp  19169  gsummptnn0fz  19371  srgbinomlem4  19558  cnfldfun  20375  cnfldfunALT  20376  cnfld1  20388  cnsubdrglem  20414  expmhm  20432  expghm  20462  psrbag0  21020  psrbagsn  21021  coe1fsupp  21135  coe1mul2  21190  evls1sca  21239  matmulr  21335  mat1dimelbas  21368  mat1f1o  21375  m2detleib  21528  smadiadetglem1  21568  pmatcollpw3fi1lem2  21684  cpmidpmatlem2  21768  cpmadumatpolylem1  21778  cayhamlem3  21784  cayhamlem4  21785  isbasis3g  21846  fctop  21901  cctop  21903  refref  22410  bl2in  23298  dscmet  23470  iihalf1  23828  iihalf2  23830  icopnfhmeo  23840  iccpnfhmeo  23842  xrhmeo  23843  iscvsi  24026  zclmncvs  24045  ncvs1  24054  ehl2eudis  24319  minveclem2  24323  minveclem4  24329  ovolunlem1a  24393  volf  24426  i1f1lem  24586  mbfi1fseqlem5  24617  dveflem  24876  pilem2  25344  pilem3  25345  sinhalfpilem  25353  sincosq1lem  25387  tangtx  25395  sinq12gt0  25397  sincos4thpi  25403  sincos6thpi  25405  sincos3rdpi  25406  pigt3  25407  pige3ALT  25409  coseq1  25414  efeq1  25417  efif1olem4  25434  angneg  25686  ang180lem1  25692  1cubrlem  25724  quart1  25739  log2cnv  25827  log2tlbnd  25828  log2ublem1  25829  log2ub  25832  emcllem1  25878  emcllem6  25883  basellem1  25963  basellem2  25964  basellem3  25965  basellem8  25970  ppiublem1  26083  ppiublem2  26084  ppiub  26085  chtublem  26092  chtub  26093  bcmono  26158  bclbnd  26161  bpos1lem  26163  bposlem1  26165  bposlem2  26166  bposlem3  26167  bposlem4  26168  bposlem5  26169  bposlem6  26170  bposlem7  26171  bposlem8  26172  bposlem9  26173  lgsdir2lem1  26206  1lgs  26221  gausslemma2dlem0c  26239  gausslemma2dlem0d  26240  gausslemma2dlem1a  26246  gausslemma2dlem2  26248  gausslemma2dlem3  26249  gausslemma2dlem5  26252  gausslemma2dlem6  26253  lgsquad2lem2  26266  2lgslem1a1  26270  2lgslem1a2  26271  2lgslem1c  26274  2lgslem3a  26277  2lgslem3b  26278  2lgslem3c  26279  2lgslem3d  26280  2lgslem3  26285  2lgsoddprmlem1  26289  addsqrexnreu  26323  addsqnreup  26324  chebbnd1lem1  26350  chebbnd1lem3  26352  chebbnd1  26353  dchrisum0flblem2  26390  dchrisum0lem1  26397  mulog2sumlem2  26416  selberglem2  26427  chpdifbndlem1  26434  ercgrg  26608  axlowdimlem4  27036  axlowdimlem5  27037  axlowdimlem6  27038  axlowdimlem7  27039  axlowdimlem8  27040  axlowdimlem10  27042  axlowdimlem11  27043  graop  27120  grastruct  27121  uhgrunop  27166  upgrop  27185  upgrunop  27210  umgrunop  27212  usgrop  27254  usgr2v1e2w  27340  usgrexmpldifpr  27346  usgrexmpledg  27350  uhgrsubgrself  27368  uhgrspan1lem1  27388  upgrres1lem1  27397  fusgrfis  27418  vtxd0nedgb  27576  p1evtxdeqlem  27600  p1evtxdeq  27601  p1evtxdp1  27602  umgr2v2e  27613  vdegp1bi  27625  wlkcomp  27718  upgr2pthnlp  27819  usgr2trlncl  27847  usgr2pthlem  27850  clwlkcomp  27866  uspgrn2crct  27892  wwlksonvtx  27939  wspthnonp  27943  2wlkond  28021  2pthond  28026  2pthon3v  28027  umgr2adedgwlkonALT  28031  umgr2wlk  28033  umgr2wlkon  28034  wpthswwlks2on  28045  elwspths2spth  28051  0ewlk  28197  0pth  28208  0pthonv  28212  1pthon2v  28236  3wlkdlem4  28245  3trlond  28256  3pthond  28258  3spthond  28260  trlsegvdeglem3  28305  eupthvdres  28318  eupth2lemb  28320  ex-natded5.2i  28489  ex-an  28505  ex-id  28517  ex-po  28518  ex-fl  28530  ex-mod  28532  ex-exp  28533  ex-lcm  28541  nvz0  28749  ipidsq  28791  ipdirilem  28910  siilem1  28932  minvecolem2  28956  minvecolem3  28957  minvecolem4  28961  hvsubcan  29155  hvsubcan2  29156  normlem7tALT  29200  helch  29324  hsn0elch  29329  hhshsslem2  29349  hhsssh  29350  shscli  29398  shintcli  29410  shintcl  29411  chintcli  29412  chintcl  29413  shincli  29443  shsval2i  29468  omlsi  29485  chincli  29541  chabs1  29597  fh1i  29702  fh2i  29703  cm2ji  29706  pjnormi  29802  nmopsetn0  29946  nmfnsetn0  29959  lnophm  30100  nmcexi  30107  nmbdfnlb  30131  imaelshi  30139  nlelshi  30141  nmopadjlem  30170  nmopcoadji  30182  hmopidmch  30234  hmopidmpj  30235  sto1i  30317  stlei  30321  stji1i  30323  csmdsymi  30415  chirred  30476  cdj3lem1  30515  rpdp2cl  30876  dp2lt10  30878  dp2lt  30879  dp2ltc  30881  dpfrac1  30886  dplti  30899  dpgti  30900  dpexpp1  30902  dpadd3  30906  dpmul  30907  dpmul4  30908  xrsclat  31008  nn0archi  31261  lmatfvlem  31479  xrge0iifmhm  31603  qqh0  31646  qqh1  31647  rerrext  31671  cnrrext  31672  prsiga  31811  oms0  31976  coinfliprv  32161  ballotlem1  32165  ballotth  32216  signsw0g  32247  hgt750lemd  32340  hgt750lem  32343  hgt750lem2  32344  hgt750leme  32350  tgoldbachgt  32355  subfacval2  32862  erdszelem2  32867  cvmliftlem4  32963  satom  33031  satfv1  33038  sat1el2xp  33054  fmlaomn0  33065  satfdmfmla  33075  satfv1fvfmla1  33098  ex-sategoelelomsuc  33101  ex-sategoelel12  33102  prv0  33105  prv1n  33106  elmrsubrn  33195  msubfval  33199  problem4  33339  quad3  33341  dfpo2  33441  br6  33443  dfon2lem3  33480  ssttrcl  33514  poxp2  33527  poseq  33539  fullfunfnv  33985  fneref  34276  filnetlem2  34305  filnetlem3  34306  onpsstopbas  34356  dnizeq0  34392  dnibndlem12  34406  knoppcnlem5  34414  knoppcnlem8  34417  knoppcnlem10  34419  knoppcnlem11  34420  knoppndvlem14  34442  cnndvlem1  34454  bj-genr  34525  bj-genl  34526  bj-genan  34527  bj-2upln1upl  34951  bj-vtoclgfALT  34967  bj-brab2a1  35055  bj-opabssvv  35056  taupilem1  35226  topdifinf  35257  sin2h  35504  cos2h  35505  tan2h  35506  poimirlem1  35515  poimirlem2  35516  poimirlem3  35517  poimirlem4  35518  poimirlem6  35520  poimirlem7  35521  poimirlem11  35525  poimirlem12  35526  poimirlem16  35530  poimirlem17  35531  poimirlem19  35533  poimirlem20  35534  poimirlem22  35536  poimirlem23  35537  poimirlem24  35538  poimirlem25  35539  poimirlem26  35540  poimirlem29  35543  poimirlem31  35545  mblfinlem3  35553  mblfinlem4  35554  ismblfin  35555  itg2addnclem2  35566  asindmre  35597  heiborlem7  35712  riscer  35883  refrelcoss3  36318  symrelcoss3  36320  ishlatiN  37106  0psubN  37500  atpsubN  37504  gcdcomnni  39731  gcdnegnni  39732  neggcdnni  39733  60gcd7e1  39747  lcmeprodgcdi  39749  lcm2un  39756  lcm3un  39757  lcmineqlem4  39774  lcmineqlem6  39776  3lexlogpow5ineq1  39796  aks4d1p1p2  39811  mzpclall  40252  diophin  40297  diophun  40298  eldioph4b  40336  irrapx1  40353  2nn0ind  40470  aomclem4  40585  ifpid3g  40784  ifpid2g  40785  ifpbi1b  40795  eu0  40812  pwinfi  40847  rtrclex  40901  cnvrcl0  40909  dfrcl2  40959  relexp1idm  40999  relexp0idm  41000  clsk1independent  41333  lhe4.4ex1a  41620  expgrowth  41626  ax6e2nd  41851  uun0.1  42071  relopabVD  42194  ax6e2ndVD  42201  sb5ALTVD  42206  ax6e2ndALT  42223  dvmptconst  43131  dvmptidg  43133  dvmulcncf  43141  dvdivcncf  43143  dvnprodlem3  43164  itgsinexplem1  43170  volioof  43203  stoweidlem13  43229  stoweidlem14  43230  stoweidlem26  43242  stoweidlem34  43250  stoweidlem49  43265  stoweidlem59  43275  dirkertrigeqlem3  43316  dirkercncflem1  43319  dirkercncflem2  43320  fourierdlem57  43379  fourierdlem62  43384  fourierdlem103  43425  fourierdlem111  43433  fourierswlem  43446  fouriersw  43447  salexct2  43553  salexct3  43556  salgencntex  43557  salgensscntex  43558  gsumge0cl  43584  sge00  43589  sge0tsms  43593  0ome  43742  ovnlecvr  43771  ovn0lem  43778  hoidmvle  43813  ovnsubadd2lem  43858  smflimlem6  43983  mbfpsssmf  43990  smfmullem4  44000  smfpimbor1lem1  44004  astbstanbst  44076  aistbistaandb  44077  abnotataxb  44083  aifftbifffaibif  44088  confun4  44109  plcofph  44111  plvcofph  44113  plvcofphax  44114  plvofpos  44115  mdandyv0  44116  mdandyv1  44117  mdandyv2  44118  mdandyv3  44119  mdandyv4  44120  mdandyv5  44121  mdandyv6  44122  mdandyv7  44123  mdandyv8  44124  mdandyv9  44125  mdandyv10  44126  mdandyv11  44127  mdandyv12  44128  mdandyv13  44129  mdandyv14  44130  mdandyv15  44131  mdandyvr0  44132  mdandyvr1  44133  mdandyvr2  44134  mdandyvr3  44135  mdandyvr4  44136  mdandyvr5  44137  mdandyvr6  44138  mdandyvr7  44139  mdandyvrx0  44148  mdandyvrx1  44149  mdandyvrx2  44150  mdandyvrx3  44151  mdandyvrx4  44152  mdandyvrx5  44153  mdandyvrx6  44154  mdandyvrx7  44155  dandysum2p2e4  44165  or2expropbilem1  44198  dfnelbr2  44437  ich2exprop  44596  paireqne  44636  fmtno4prmfac  44697  31prm  44722  lighneallem4a  44733  41prothprmlem2  44743  zofldiv2ALTV  44787  nfermltl8rev  44867  nfermltl2rev  44868  nfermltlrev  44869  gbegt5  44886  gbowgt5  44887  gboge9  44889  9gbo  44899  11gbo  44900  nnsum3primes4  44913  nnsum3primesgbe  44917  nnsum4primesodd  44921  nnsum4primesoddALTV  44922  nnsum4primeseven  44925  nnsum4primesevenALTV  44926  tgblthelfgott  44940  tgoldbach  44942  isomgrref  44960  ushrisomgr  44966  nn0mnd  45046  mgmplusgiopALT  45061  sgrp2sgrp  45095  isrnghm  45123  2zrngaabl  45175  rnghmsscmap2  45204  rnghmsscmap  45205  funcrngcsetc  45229  funcrngcsetcALT  45230  rhmsscmap2  45250  rhmsscmap  45251  funcringcsetc  45266  funcringcsetcALTV2lem8  45274  funcringcsetclem8ALTV  45297  zlmodzxzlmod  45363  zlmodzxzel  45364  zlmodzxzscm  45366  zlmodzxzadd  45367  snlindsntorlem  45484  ldepspr  45487  lmod1lem2  45502  lmod1lem3  45503  lmod1lem4  45504  lmod1lem5  45505  lmodn0  45509  zlmodzxznm  45511  zlmodzxzldeplem  45512  zlmodzxzldeplem1  45514  zlmodzxzldeplem3  45516  lvecpsslmod  45521  ldepsnlinc  45522  ldepslinc  45523  expnegico01  45532  zofldiv2  45550  flnn0div2ge  45552  elbigo2  45571  nnlog2ge0lt1  45585  digfval  45616  dignnld  45622  dignn0flhalf  45637  2arymaptfo  45673  itcovalt2lem1  45694  prelrrx2  45732  eenglngeehlnmlem2  45757  rrxsphere  45767  line2  45771  line2x  45773  line2y  45774  itsclc0yqsollem2  45782  inlinecirc02plem  45805  sepfsepc  45894  alimp-surprise  46155  aacllem  46176