Theorem pm3.2i 470

Description: Infer conjunction of premises. (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 462	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
4	1, 2, 3	mp2 9	1 ⊢ (𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  pm4.87  606  dfbi  659  mp4an  705  3pm3.2i  1232  unssi  3750  elini  3759  ssini  3798  bm1.3ii  4712  epelg  4950  elvv  5100  relopabi  5167  funpr  5858  funcnvpr  5864  mpt2v  6648  caovcom  6729  1st2val  7085  2nd2val  7086  elxp7  7092  wfrlem13  7314  wfr3  7322  tfr1a  7377  oeoa  7564  oeoe  7566  erov  7731  endisj  7932  phplem2  8025  snopfsupp  8181  r1funlim  8512  dfac2  8836  cflecard  8958  canth4  9348  canthnumlem  9349  canthwelem  9351  canthp1lem2  9354  pwfseqlem4  9363  wunex3  9442  addsrpr  9775  mulsrpr  9776  recexsrlem  9803  mulcani  10545  div1  10595  recdiv  10610  divdiv1  10615  divdiv2  10616  div23i  10662  div11i  10663  divmuldivi  10664  divadddivi  10666  divdivdivi  10667  lemulge11  10764  negiso  10880  dfnn3  10911  2cnne0  11119  2rene0  11120  halfpm6th  11130  avglt1  11147  avglt2  11148  div4p1lem1div2  11164  3halfnz  11332  divlt1lt  11775  divle1le  11776  nnledivrp  11816  x2times  12001  xrsupsslem  12009  xrinfmsslem  12010  fz0to4untppr  12311  fldiv4lem1div2uz2  12499  om2uzoi  12616  fzennn  12629  expge1  12759  sqoddm1div8  12890  faclbnd2  12940  faclbnd4lem1  12942  4bc2eq6  12978  hashfxnn0  12986  hashfOLD  12988  hashsnlei  13067  hashunlei  13072  hashsslei  13073  hash2prb  13111  repswccat  13383  cshwsexa  13421  funcnvs4  13510  f1oun2prg  13512  wrdlen2i  13534  relexpaddg  13641  cjreb  13711  sqrt2gt1lt2  13863  abs1m  13923  amgm2  13957  climcndslem2  14421  fprodn0f  14561  bpoly3  14628  efcllem  14647  ege2le3  14659  efi4p  14706  efival  14721  sin01bnd  14754  cos01bnd  14755  cos1bnd  14756  cos2bnd  14757  sin01gt0  14759  cos01gt0  14760  sin02gt0  14761  sincos2sgn  14763  sin4lt0  14764  egt2lt3  14773  rpnnen2lem3  14784  rpnnen2lem11  14792  nthruc  14819  nthruz  14820  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  mod2eq1n2dvds  14909  oddge22np1  14911  halfleoddlt  14924  nno  14936  divalglem5  14958  ndvdsi  14974  flodddiv4  14975  flodddiv4lt  14977  flodddiv4t2lthalf  14978  bitsp1o  14993  3lcm2e6woprm  15166  6lcm4e12  15167  pcrec  15401  prmrec  15464  prmo1  15579  prmgaplcmlem1  15593  prmgaplcm  15602  modsubi  15614  structfn  15708  strlemor0  15795  strlemor1  15796  strleun  15799  isofn  16258  sscres  16306  funcestrcsetclem7  16609  funcestrcsetclem8  16610  fullestrcsetc  16614  mgmnsgrpex  17241  ga0  17554  symg2bas  17641  f1otrspeq  17690  psgnsn  17763  0frgp  18015  gsummptnn0fz  18205  srgbinomlem4  18366  psrbag0  19315  psrbagsn  19316  coe1fsupp  19405  coe1mul2  19460  evls1sca  19509  cnfld1  19590  cnsubdrglem  19616  expmhm  19634  expghm  19663  matmulr  20063  mat1dimelbas  20096  mat1f1o  20103  m2detleib  20256  smadiadetglem1  20296  pmatcollpw3fi1lem2  20411  cpmidpmatlem2  20495  cpmadumatpolylem1  20505  cayhamlem3  20511  cayhamlem4  20512  isbasis3g  20564  fctop  20618  cctop  20620  refref  21126  bl2in  22015  dscmet  22187  iihalf1  22538  iihalf2  22540  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  iscvsi  22737  zclmncvs  22756  ncvs1  22765  minveclem2  23005  minveclem4  23011  ovolunlem1a  23071  volf  23104  i1f1lem  23262  mbfi1fseqlem5  23292  dveflem  23546  pilem2  24010  pilem3  24011  sinhalfpilem  24019  sincosq1lem  24053  tangtx  24061  sinq12gt0  24063  sincos4thpi  24069  sincos6thpi  24071  sincos3rdpi  24072  pige3  24073  coseq1  24078  efeq1  24079  efif1olem4  24095  logblog  24330  angneg  24333  ang180lem1  24339  1cubrlem  24368  quart1  24383  log2cnv  24471  log2tlbnd  24472  log2ublem1  24473  log2ub  24476  emcllem1  24522  emcllem6  24527  basellem1  24607  basellem2  24608  basellem3  24609  basellem8  24614  ppiublem1  24727  ppiublem2  24728  ppiub  24729  chtublem  24736  chtub  24737  bcmono  24802  bclbnd  24805  bpos1lem  24807  bposlem1  24809  bposlem2  24810  bposlem3  24811  bposlem4  24812  bposlem5  24813  bposlem6  24814  bposlem7  24815  bposlem8  24816  bposlem9  24817  lgsdir2lem1  24850  1lgs  24865  gausslemma2dlem0c  24883  gausslemma2dlem0d  24884  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  gausslemma2dlem3  24893  gausslemma2dlem5  24896  gausslemma2dlem6  24897  lgsquad2lem2  24910  2lgslem1a1  24914  2lgslem1a2  24915  2lgslem1c  24918  2lgslem3a  24921  2lgslem3b  24922  2lgslem3c  24923  2lgslem3d  24924  2lgslem3  24929  2lgsoddprmlem1  24933  chebbnd1lem1  24958  chebbnd1lem3  24960  chebbnd1  24961  dchrisum0flblem2  24998  dchrisum0lem1  25005  mulog2sumlem2  25024  selberglem2  25035  chpdifbndlem1  25042  ercgrg  25212  axlowdimlem4  25625  axlowdimlem5  25626  axlowdimlem6  25627  axlowdimlem7  25628  axlowdimlem8  25629  axlowdimlem10  25631  axlowdimlem11  25632  structvtxvallem  25697  graop  25706  grastruct  25707  uhgrunop  25741  upgrunop  25785  umgrunop  25787  usgraexmpldifpr  25928  usgraexmpledg  25932  wlkcomp  26053  0trl  26076  2trllemH  26082  2trllemE  26083  2wlklemA  26084  2wlklemB  26085  2wlklemC  26086  wlkntrllem2  26090  wlkntrl  26092  0pth  26100  0pthonv  26111  constr1trl  26118  1pthon  26121  1pthon2v  26123  constr2spth  26130  constr2pth  26131  2pthon  26132  2pthon3v  26134  usgra2adedgspth  26141  usgra2adedgwlk  26142  usgra2adedgwlkon  26143  usg2wlk  26145  usg2wlkon  26146  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  constr3lem1  26173  constr3lem4  26175  constr3trllem3  26180  constr3pthlem2  26184  clwlkcomp  26291  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  usg2wlkonot  26410  usg2wotspth  26411  frgraregord013  26645  ex-natded5.2i  26655  ex-an  26671  ex-id  26683  ex-po  26684  ex-fl  26696  ex-mod  26698  ex-exp  26699  ex-lcm  26707  nvz0  26907  ipidsq  26949  ipdirilem  27068  siilem1  27090  minvecolem2  27115  minvecolem3  27116  minvecolem4  27120  hvsubcan  27315  hvsubcan2  27316  normlem7tALT  27360  helch  27484  hsn0elch  27489  hhshsslem2  27509  hhsssh  27510  shscli  27560  shintcli  27572  shintcl  27573  chintcli  27574  chintcl  27575  shincli  27605  shsval2i  27630  omlsi  27647  chincli  27703  chabs1  27759  fh1i  27864  fh2i  27865  cm2ji  27868  pjnormi  27964  nmopsetn0  28108  nmfnsetn0  28121  lnophm  28262  nmcexi  28269  nmbdfnlb  28293  imaelshi  28301  nlelshi  28303  nmopadjlem  28332  nmopcoadji  28344  hmopidmch  28396  hmopidmpj  28397  sto1i  28479  stlei  28483  stji1i  28485  csmdsymi  28577  chirred  28638  cdj3lem1  28677  xrsclat  29011  nn0archi  29174  lmatfvlem  29209  xrge0iifmhm  29313  qqh0  29356  qqh1  29357  rerrext  29381  cnrrext  29382  prsiga  29521  oms0  29686  coinfliprv  29871  ballotlem1  29875  ballotth  29926  signsw0g  29959  subfacval2  30423  erdszelem2  30428  cvmliftlem4  30524  elmrsubrn  30671  msubfval  30675  problem4  30816  quad3  30818  dfpo2  30898  br6  30900  dfon2lem3  30934  poseq  30994  fullfunfnv  31223  fneref  31515  filnetlem2  31544  filnetlem3  31545  onpsstopbas  31599  dnizeq0  31635  dnibndlem12  31649  knoppcnlem5  31657  knoppcnlem8  31660  knoppcnlem10  31662  knoppcnlem11  31663  knoppndvlem14  31686  cnndvlem1  31698  bj-genr  31776  bj-genl  31777  bj-genan  31778  bj-2upln1upl  32205  bj-vtoclgfALT  32212  bj-toprntopon  32244  bj-pwnex  32246  taupilem1  32344  topdifinf  32373  sin2h  32569  cos2h  32570  tan2h  32571  pigt3  32572  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem29  32608  poimirlem31  32610  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnclem2  32632  asindmre  32665  heiborlem7  32786  riscer  32957  ac6s6f  33151  ishlatiN  33660  0psubN  34053  atpsubN  34057  mzpclall  36308  diophin  36354  diophun  36355  eldioph4b  36393  irrapx1  36410  2nn0ind  36528  aomclem4  36645  ifpid3g  36856  ifpid2g  36857  ifpbi1b  36867  pwinfi  36888  rtrclex  36943  cnvrcl0  36951  dfrcl2  36985  relexp1idm  37025  relexp0idm  37026  clsk1independent  37364  lhe4.4ex1a  37550  expgrowth  37556  ax6e2nd  37795  uun0.1  38026  relopabVD  38159  ax6e2ndVD  38166  sb5ALTVD  38171  ax6e2ndALT  38188  fnchoice  38211  dvmptconst  38803  dvmptidg  38805  dvmulcncf  38815  dvdivcncf  38817  dvnprodlem3  38838  itgsinexplem1  38845  volioof  38880  stoweidlem13  38906  stoweidlem14  38907  stoweidlem26  38919  stoweidlem34  38927  stoweidlem49  38942  stoweidlem59  38952  dirkertrigeqlem3  38993  dirkercncflem1  38996  dirkercncflem2  38997  fourierdlem57  39056  fourierdlem62  39061  fourierdlem103  39102  fourierdlem111  39110  fourierswlem  39123  fouriersw  39124  salexct2  39233  salexct3  39236  salgencntex  39237  salgensscntex  39238  gsumge0cl  39264  sge00  39269  sge0tsms  39273  0ome  39419  ovnlecvr  39448  ovn0lem  39455  hoidmvle  39490  ovnsubadd2lem  39535  smflimlem6  39662  mbfpsssmf  39669  smfmullem4  39679  smfpimbor1lem1  39683  astbstanbst  39725  aistbistaandb  39726  abnotataxb  39732  aifftbifffaibif  39737  confun4  39758  plcofph  39760  plvcofph  39762  plvcofphax  39763  plvofpos  39764  mdandyv0  39765  mdandyv1  39766  mdandyv2  39767  mdandyv3  39768  mdandyv4  39769  mdandyv5  39770  mdandyv6  39771  mdandyv7  39772  mdandyv8  39773  mdandyv9  39774  mdandyv10  39775  mdandyv11  39776  mdandyv12  39777  mdandyv13  39778  mdandyv14  39779  mdandyv15  39780  mdandyvr0  39781  mdandyvr1  39782  mdandyvr2  39783  mdandyvr3  39784  mdandyvr4  39785  mdandyvr5  39786  mdandyvr6  39787  mdandyvr7  39788  mdandyvrx0  39797  mdandyvrx1  39798  mdandyvrx2  39799  mdandyvrx3  39800  mdandyvrx4  39801  mdandyvrx5  39802  mdandyvrx6  39803  mdandyvrx7  39804  dandysum2p2e4  39814  fmtno4prmfac  40022  31prm  40050  lighneallem4a  40063  41prothprmlem2  40073  zofldiv2ALTV  40112  gbegt5  40183  gbogt5  40184  gboage9  40186  9gboa  40196  11gboa  40197  nnsum3primes4  40204  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  tgblthelfgott  40229  tgoldbach  40232  tgblthelfgottOLD  40236  tgoldbachOLD  40239  pfx2  40275  mptmpt2opabbrd  40335  usgrop  40393  usgr2v1e2w  40478  usgrexmpledg  40486  uhgrsubgrself  40504  uhgrspan1lem1  40524  upgrres1lem1  40528  fusgrfis  40549  vtxd0nedgb  40703  p1evtxdeqlem  40728  p1evtxdeq  40729  p1evtxdp1  40730  umgr2v2e  40741  vdegp1bi-av  40753  1wlkcomp  40835  upgr2pthnlp  40938  usgr2trlncl  40966  usgr2pthlem  40969  clWlkcomp  40986  uspgrn2crct  41011  wspthnonp  41055  21wlkond  41144  2pthond  41149  2pthon3v-av  41150  umgr2adedgwlkonALT  41154  umgr2wlk  41156  umgr2wlkon  41157  umgrwwlks2on  41161  wpthswwlks2on  41164  elwspths2spth  41171  0ewlk  41282  0pth-av  41293  0pthonv-av  41297  1pthon2v-av  41320  31wlkdlem4  41329  3trlond  41340  3pthond  41342  3spthond  41344  trlsegvdeglem3  41390  eupthvdres  41403  eupth2lemb  41405  mgmplusgiopALT  41620  sgrp2sgrp  41654  isrnghm  41682  2zrngaabl  41734  rnghmsscmap2  41765  rnghmsscmap  41766  funcrngcsetc  41790  funcrngcsetcALT  41791  rhmsscmap2  41811  rhmsscmap  41812  funcringcsetc  41827  funcringcsetcALTV2lem8  41835  funcringcsetclem8ALTV  41858  zlmodzxzlmod  41925  zlmodzxzel  41926  zlmodzxzscm  41928  zlmodzxzadd  41929  snlindsntorlem  42053  ldepspr  42056  lmod1lem2  42071  lmod1lem3  42072  lmod1lem4  42073  lmod1lem5  42074  lmodn0  42078  zlmodzxznm  42080  zlmodzxzldeplem  42081  zlmodzxzldeplem1  42083  zlmodzxzldeplem3  42085  lvecpsslmod  42090  ldepsnlinc  42091  ldepslinc  42092  expnegico01  42102  zofldiv2  42119  flnn0div2ge  42121  elbigo2  42144  nnlog2ge0lt1  42158  digfval  42189  dignnld  42195  dignn0flhalf  42210  dpfrac1  42312  dpfrac1OLD  42313  alimp-surprise  42335  aacllem  42356