Theorem pm3.2i 471

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

Syntax hints:   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mp4an  689  pm4.87  838  3pm3.2i  1332  unssi  4082  ssini  4128  opthhausdorff  5298  epelgOLD  5355  elvv  5512  relopabiv  5579  relopabi  5580  funpr  6280  funcnvpr  6286  mpov  7120  caovcom  7201  snnex  7337  pwnex  7338  1st2val  7573  2nd2val  7574  elxp7  7580  opreuopreu  7590  mptmpoopabbrd  7634  wfrlem13  7819  wfr3  7827  tfr1a  7882  oeoa  8073  oeoe  8075  erov  8244  endisj  8451  phplem2  8544  snopfsupp  8702  r1funlim  9041  dfac2b  9402  cflecard  9521  canth4  9915  canthnumlem  9916  canthwelem  9918  canthp1lem2  9921  pwfseqlem4  9930  wunex3  10009  addsrpr  10343  mulsrpr  10344  recexsrlem  10371  mulcani  11127  div1  11177  recdiv  11194  divdiv1  11199  divdiv2  11200  div23i  11246  div11i  11247  divmuldivi  11248  divadddivi  11250  divdivdivi  11251  lemulge11  11350  negiso  11469  dfnn3  11500  2cnne0  11695  2rene0  11696  halfpm6th  11706  avglt1  11723  avglt2  11724  div4p1lem1div2  11740  3halfnz  11910  divlt1lt  12308  divle1le  12309  nnledivrp  12351  x2times  12542  xrsupsslem  12550  xrinfmsslem  12551  fz0to4untppr  12860  om2uzoi  13173  fzennn  13186  expge1  13316  sqoddm1div8  13454  faclbnd2  13501  faclbnd4lem1  13503  4bc2eq6  13539  hashfxnn0  13547  hashsnlei  13627  hashunlei  13634  hashsslei  13635  hash2prb  13676  repswccat  13984  cshwsexa  14022  funcnvs4  14113  f1oun2prg  14115  wrdlen2i  14140  pfx2  14145  relexpaddg  14246  cjreb  14316  sqrt2gt1lt2  14468  abs1m  14529  bpoly3  15245  ege2le3  15276  efi4p  15323  efival  15338  sin01bnd  15371  cos01bnd  15372  cos1bnd  15373  cos2bnd  15374  sin01gt0  15376  cos01gt0  15377  sin02gt0  15378  sincos2sgn  15380  sin4lt0  15381  egt2lt3  15392  rpnnen2lem3  15402  rpnnen2lem11  15410  nthruc  15438  nthruz  15439  3dvdsdec  15514  3dvds2dec  15515  mod2eq1n2dvds  15529  halfleoddlt  15544  divalglem5  15581  ndvdsi  15596  flodddiv4  15597  flodddiv4lt  15599  bitsp1o  15615  3lcm2e6woprm  15788  6lcm4e12  15789  pcrec  16024  prmrec  16087  prmgaplcmlem1  16216  prmgaplcm  16225  modsubi  16237  structfn  16329  strleun  16420  isofn  16874  sscres  16922  funcestrcsetclem7  17225  funcestrcsetclem8  17226  fullestrcsetc  17230  mgmnsgrpex  17857  ga0  18169  symg2bas  18257  f1otrspeq  18306  psgnsn  18379  0frgp  18632  gsummptnn0fz  18823  srgbinomlem4  18983  psrbag0  19961  psrbagsn  19962  coe1fsupp  20065  coe1mul2  20120  evls1sca  20169  cnfldfun  20239  cnfldfunALT  20240  cnfld1  20252  cnsubdrglem  20278  expmhm  20296  expghm  20325  matmulr  20731  mat1dimelbas  20764  mat1f1o  20771  m2detleib  20924  smadiadetglem1  20964  pmatcollpw3fi1lem2  21079  cpmidpmatlem2  21163  cpmadumatpolylem1  21173  cayhamlem3  21179  cayhamlem4  21180  isbasis3g  21241  fctop  21296  cctop  21298  refref  21805  bl2in  22693  dscmet  22865  iihalf1  23218  iihalf2  23220  icopnfhmeo  23230  iccpnfhmeo  23232  xrhmeo  23233  iscvsi  23416  zclmncvs  23435  ncvs1  23444  ehl2eudis  23708  minveclem2  23712  minveclem4  23718  ovolunlem1a  23780  volf  23813  i1f1lem  23973  mbfi1fseqlem5  24003  dveflem  24259  pilem2  24723  pilem3  24724  sinhalfpilem  24732  sincosq1lem  24766  tangtx  24774  sinq12gt0  24776  sincos4thpi  24782  sincos6thpi  24784  sincos3rdpi  24785  pigt3  24786  pige3ALT  24788  coseq1  24793  efeq1  24794  efif1olem4  24810  angneg  25062  ang180lem1  25068  1cubrlem  25100  quart1  25115  log2cnv  25204  log2tlbnd  25205  log2ublem1  25206  log2ub  25209  emcllem1  25255  emcllem6  25260  basellem1  25340  basellem2  25341  basellem3  25342  basellem8  25347  ppiublem1  25460  ppiublem2  25461  ppiub  25462  chtublem  25469  chtub  25470  bcmono  25535  bclbnd  25538  bpos1lem  25540  bposlem1  25542  bposlem2  25543  bposlem3  25544  bposlem4  25545  bposlem5  25546  bposlem6  25547  bposlem7  25548  bposlem8  25549  bposlem9  25550  lgsdir2lem1  25583  1lgs  25598  gausslemma2dlem0c  25616  gausslemma2dlem0d  25617  gausslemma2dlem1a  25623  gausslemma2dlem2  25625  gausslemma2dlem3  25626  gausslemma2dlem5  25629  gausslemma2dlem6  25630  lgsquad2lem2  25643  2lgslem1a1  25647  2lgslem1a2  25648  2lgslem1c  25651  2lgslem3a  25654  2lgslem3b  25655  2lgslem3c  25656  2lgslem3d  25657  2lgslem3  25662  2lgsoddprmlem1  25666  addsqrexnreu  25700  addsqnreup  25701  chebbnd1lem1  25727  chebbnd1lem3  25729  chebbnd1  25730  dchrisum0flblem2  25767  dchrisum0lem1  25774  mulog2sumlem2  25793  selberglem2  25804  chpdifbndlem1  25811  ercgrg  25985  axlowdimlem4  26414  axlowdimlem5  26415  axlowdimlem6  26416  axlowdimlem7  26417  axlowdimlem8  26418  axlowdimlem10  26420  axlowdimlem11  26421  graop  26497  grastruct  26498  uhgrunop  26543  upgrop  26562  upgrunop  26587  umgrunop  26589  usgrop  26631  usgr2v1e2w  26717  usgrexmpldifpr  26723  usgrexmpledg  26727  uhgrsubgrself  26745  uhgrspan1lem1  26765  upgrres1lem1  26774  fusgrfis  26795  vtxd0nedgb  26953  p1evtxdeqlem  26977  p1evtxdeq  26978  p1evtxdp1  26979  umgr2v2e  26990  vdegp1bi  27002  wlkcomp  27095  upgr2pthnlp  27200  usgr2trlncl  27228  usgr2pthlem  27231  clwlkcomp  27247  uspgrn2crct  27273  wwlksonvtx  27320  wspthnonp  27324  2wlkond  27403  2pthond  27408  2pthon3v  27409  umgr2adedgwlkonALT  27413  umgr2wlk  27415  umgr2wlkon  27416  wpthswwlks2on  27427  elwspths2spth  27433  0ewlk  27580  0pth  27591  0pthonv  27595  1pthon2v  27619  3wlkdlem4  27628  3trlond  27639  3pthond  27641  3spthond  27643  trlsegvdeglem3  27689  eupthvdres  27702  eupth2lemb  27704  ex-natded5.2i  27877  ex-an  27893  ex-id  27905  ex-po  27906  ex-fl  27918  ex-mod  27920  ex-exp  27921  ex-lcm  27929  nvz0  28136  ipidsq  28178  ipdirilem  28297  siilem1  28319  minvecolem2  28343  minvecolem3  28344  minvecolem4  28348  hvsubcan  28542  hvsubcan2  28543  normlem7tALT  28587  helch  28711  hsn0elch  28716  hhshsslem2  28736  hhsssh  28737  shscli  28785  shintcli  28797  shintcl  28798  chintcli  28799  chintcl  28800  shincli  28830  shsval2i  28855  omlsi  28872  chincli  28928  chabs1  28984  fh1i  29089  fh2i  29090  cm2ji  29093  pjnormi  29189  nmopsetn0  29333  nmfnsetn0  29346  lnophm  29487  nmcexi  29494  nmbdfnlb  29518  imaelshi  29526  nlelshi  29528  nmopadjlem  29557  nmopcoadji  29569  hmopidmch  29621  hmopidmpj  29622  sto1i  29704  stlei  29708  stji1i  29710  csmdsymi  29802  chirred  29863  cdj3lem1  29902  rpdp2cl  30242  dp2lt10  30244  dp2lt  30245  dp2ltc  30247  dpfrac1  30252  dplti  30265  dpgti  30266  dpexpp1  30268  dpadd3  30272  dpmul  30273  dpmul4  30274  xrsclat  30341  nn0archi  30570  lmatfvlem  30695  xrge0iifmhm  30799  qqh0  30842  qqh1  30843  rerrext  30867  cnrrext  30868  prsiga  31007  oms0  31172  coinfliprv  31357  ballotlem1  31361  ballotth  31412  signsw0g  31443  hgt750lemd  31536  hgt750lem  31539  hgt750lem2  31540  hgt750leme  31546  tgoldbachgt  31551  subfacval2  32043  erdszelem2  32048  cvmliftlem4  32144  satom  32212  satfv1  32219  sat1el2xp  32235  fmlaomn0  32246  satfdmfmla  32256  satfv1fvfmla1  32279  ex-sategoelelomsuc  32282  ex-sategoelel12  32283  prv0  32286  prv1n  32287  elmrsubrn  32376  msubfval  32380  problem4  32520  quad3  32522  dfpo2  32600  br6  32602  dfon2lem3  32639  poseq  32705  fullfunfnv  33017  fneref  33308  filnetlem2  33337  filnetlem3  33338  onpsstopbas  33388  dnizeq0  33424  dnibndlem12  33438  knoppcnlem5  33446  knoppcnlem8  33449  knoppcnlem10  33451  knoppcnlem11  33452  knoppndvlem14  33474  cnndvlem1  33486  bj-genr  33549  bj-genl  33550  bj-genan  33551  bj-2upln1upl  33960  bj-vtoclgfALT  33969  taupilem1  34152  topdifinf  34180  sin2h  34432  cos2h  34433  tan2h  34434  poimirlem1  34443  poimirlem2  34444  poimirlem3  34445  poimirlem4  34446  poimirlem6  34448  poimirlem7  34449  poimirlem11  34453  poimirlem12  34454  poimirlem16  34458  poimirlem17  34459  poimirlem19  34461  poimirlem20  34462  poimirlem22  34464  poimirlem23  34465  poimirlem24  34466  poimirlem25  34467  poimirlem26  34468  poimirlem29  34471  poimirlem31  34473  mblfinlem3  34481  mblfinlem4  34482  ismblfin  34483  itg2addnclem2  34494  asindmre  34527  heiborlem7  34646  riscer  34817  refrelcoss3  35253  symrelcoss3  35255  ishlatiN  36041  0psubN  36435  atpsubN  36439  mzpclall  38828  diophin  38873  diophun  38874  eldioph4b  38912  irrapx1  38929  2nn0ind  39046  aomclem4  39161  ifpid3g  39362  ifpid2g  39363  ifpbi1b  39373  eu0  39390  pwinfi  39427  rtrclex  39481  cnvrcl0  39489  dfrcl2  39523  relexp1idm  39563  relexp0idm  39564  clsk1independent  39900  lhe4.4ex1a  40218  expgrowth  40224  ax6e2nd  40450  uun0.1  40670  relopabVD  40793  ax6e2ndVD  40800  sb5ALTVD  40805  ax6e2ndALT  40822  limsuppnfdlem  41543  dvmptconst  41760  dvmptidg  41762  dvmulcncf  41771  dvdivcncf  41773  dvnprodlem3  41794  itgsinexplem1  41800  volioof  41834  stoweidlem13  41860  stoweidlem14  41861  stoweidlem26  41873  stoweidlem34  41881  stoweidlem49  41896  stoweidlem59  41906  dirkertrigeqlem3  41947  dirkercncflem1  41950  dirkercncflem2  41951  fourierdlem57  42010  fourierdlem62  42015  fourierdlem103  42056  fourierdlem111  42064  fourierswlem  42077  fouriersw  42078  salexct2  42184  salexct3  42187  salgencntex  42188  salgensscntex  42189  gsumge0cl  42215  sge00  42220  sge0tsms  42224  0ome  42373  ovnlecvr  42402  ovn0lem  42409  hoidmvle  42444  ovnsubadd2lem  42489  smflimlem6  42614  mbfpsssmf  42621  smfmullem4  42631  smfpimbor1lem1  42635  astbstanbst  42706  aistbistaandb  42707  abnotataxb  42713  aifftbifffaibif  42718  confun4  42739  plcofph  42741  plvcofph  42743  plvcofphax  42744  plvofpos  42745  mdandyv0  42746  mdandyv1  42747  mdandyv2  42748  mdandyv3  42749  mdandyv4  42750  mdandyv5  42751  mdandyv6  42752  mdandyv7  42753  mdandyv8  42754  mdandyv9  42755  mdandyv10  42756  mdandyv11  42757  mdandyv12  42758  mdandyv13  42759  mdandyv14  42760  mdandyv15  42761  mdandyvr0  42762  mdandyvr1  42763  mdandyvr2  42764  mdandyvr3  42765  mdandyvr4  42766  mdandyvr5  42767  mdandyvr6  42768  mdandyvr7  42769  mdandyvrx0  42778  mdandyvrx1  42779  mdandyvrx2  42780  mdandyvrx3  42781  mdandyvrx4  42782  mdandyvrx5  42783  mdandyvrx6  42784  mdandyvrx7  42785  dandysum2p2e4  42795  or2expropbilem1  42803  dfnelbr2  43008  ich2exprop  43135  paireqne  43175  fmtno4prmfac  43236  31prm  43262  lighneallem4a  43275  41prothprmlem2  43285  zofldiv2ALTV  43329  nfermltl8rev  43409  nfermltl2rev  43410  nfermltlrev  43411  gbegt5  43428  gbowgt5  43429  gboge9  43431  9gbo  43441  11gbo  43442  nnsum3primes4  43455  nnsum3primesgbe  43459  nnsum4primesodd  43463  nnsum4primesoddALTV  43464  nnsum4primeseven  43467  nnsum4primesevenALTV  43468  tgblthelfgott  43482  tgoldbach  43484  isomgrref  43502  ushrisomgr  43508  mgmplusgiopALT  43599  sgrp2sgrp  43633  isrnghm  43661  2zrngaabl  43713  rnghmsscmap2  43742  rnghmsscmap  43743  funcrngcsetc  43767  funcrngcsetcALT  43768  rhmsscmap2  43788  rhmsscmap  43789  funcringcsetc  43804  funcringcsetcALTV2lem8  43812  funcringcsetclem8ALTV  43835  zlmodzxzlmod  43900  zlmodzxzel  43901  zlmodzxzscm  43903  zlmodzxzadd  43904  snlindsntorlem  44025  ldepspr  44028  lmod1lem2  44043  lmod1lem3  44044  lmod1lem4  44045  lmod1lem5  44046  lmodn0  44050  zlmodzxznm  44052  zlmodzxzldeplem  44053  zlmodzxzldeplem1  44055  zlmodzxzldeplem3  44057  lvecpsslmod  44062  ldepsnlinc  44063  ldepslinc  44064  expnegico01  44074  zofldiv2  44092  flnn0div2ge  44094  elbigo2  44113  nnlog2ge0lt1  44127  digfval  44158  dignnld  44164  dignn0flhalf  44179  prelrrx2  44201  eenglngeehlnmlem2  44226  rrxsphere  44236  line2  44240  line2x  44242  line2y  44243  itsclc0yqsollem2  44251  inlinecirc02plem  44274  alimp-surprise  44381  aacllem  44402