Theorem pm3.2i 473

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

Syntax hints:   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mp4an  691  pm4.87  839  3pm3.2i  1335  unssi  4161  ssini  4208  opthhausdorff  5407  epelgOLD  5467  elvv  5626  relopabiv  5693  relopabi  5694  funpr  6410  funcnvpr  6416  mpov  7264  caovcom  7345  snnex  7480  pwnex  7481  1st2val  7717  2nd2val  7718  elxp7  7724  opreuopreu  7734  mptmpoopabbrd  7778  wfrlem13  7967  wfr3  7975  tfr1a  8030  oeoa  8223  oeoe  8225  erov  8394  endisj  8604  phplem2  8697  snopfsupp  8856  r1funlim  9195  dfac2b  9556  cflecard  9675  canth4  10069  canthnumlem  10070  canthwelem  10072  canthp1lem2  10075  pwfseqlem4  10084  wunex3  10163  addsrpr  10497  mulsrpr  10498  recexsrlem  10525  mulcani  11279  div1  11329  recdiv  11346  divdiv1  11351  divdiv2  11352  div23i  11398  div11i  11399  divmuldivi  11400  divadddivi  11402  divdivdivi  11403  lemulge11  11502  negiso  11621  dfnn3  11652  2cnne0  11848  2rene0  11849  halfpm6th  11859  avglt1  11876  avglt2  11877  div4p1lem1div2  11893  3halfnz  12062  divlt1lt  12459  divle1le  12460  nnledivrp  12502  x2times  12693  xrsupsslem  12701  xrinfmsslem  12702  fz0to4untppr  13011  om2uzoi  13324  fzennn  13337  expge1  13467  sqoddm1div8  13605  faclbnd2  13652  faclbnd4lem1  13654  4bc2eq6  13690  hashfxnn0  13698  hashsnlei  13780  hashunlei  13787  hashsslei  13788  hash2prb  13831  repswccat  14148  cshwsexa  14186  funcnvs4  14277  f1oun2prg  14279  wrdlen2i  14304  relexpaddg  14412  cjreb  14482  sqrt2gt1lt2  14634  abs1m  14695  bpoly3  15412  ege2le3  15443  efi4p  15490  efival  15505  sin01bnd  15538  cos01bnd  15539  cos1bnd  15540  cos2bnd  15541  sin01gt0  15543  cos01gt0  15544  sin02gt0  15545  sincos2sgn  15547  sin4lt0  15548  egt2lt3  15559  rpnnen2lem3  15569  rpnnen2lem11  15577  nthruc  15605  nthruz  15606  3dvdsdec  15681  3dvds2dec  15682  mod2eq1n2dvds  15696  halfleoddlt  15711  divalglem5  15748  ndvdsi  15763  flodddiv4  15764  flodddiv4lt  15766  bitsp1o  15782  3lcm2e6woprm  15959  6lcm4e12  15960  pcrec  16195  prmrec  16258  prmgaplcmlem1  16387  prmgaplcm  16396  modsubi  16408  structfn  16500  strleun  16591  isofn  17045  sscres  17093  funcestrcsetclem7  17396  funcestrcsetclem8  17397  fullestrcsetc  17401  mgmnsgrpex  18096  pwmnd  18102  ga0  18428  symg2bas  18521  f1otrspeq  18575  psgnsn  18648  0frgp  18905  gsummptnn0fz  19106  srgbinomlem4  19293  psrbag0  20274  psrbagsn  20275  coe1fsupp  20382  coe1mul2  20437  evls1sca  20486  cnfldfun  20557  cnfldfunALT  20558  cnfld1  20570  cnsubdrglem  20596  expmhm  20614  expghm  20643  matmulr  21047  mat1dimelbas  21080  mat1f1o  21087  m2detleib  21240  smadiadetglem1  21280  pmatcollpw3fi1lem2  21395  cpmidpmatlem2  21479  cpmadumatpolylem1  21489  cayhamlem3  21495  cayhamlem4  21496  isbasis3g  21557  fctop  21612  cctop  21614  refref  22121  bl2in  23010  dscmet  23182  iihalf1  23535  iihalf2  23537  icopnfhmeo  23547  iccpnfhmeo  23549  xrhmeo  23550  iscvsi  23733  zclmncvs  23752  ncvs1  23761  ehl2eudis  24025  minveclem2  24029  minveclem4  24035  ovolunlem1a  24097  volf  24130  i1f1lem  24290  mbfi1fseqlem5  24320  dveflem  24576  pilem2  25040  pilem3  25041  sinhalfpilem  25049  sincosq1lem  25083  tangtx  25091  sinq12gt0  25093  sincos4thpi  25099  sincos6thpi  25101  sincos3rdpi  25102  pigt3  25103  pige3ALT  25105  coseq1  25110  efeq1  25113  efif1olem4  25129  angneg  25381  ang180lem1  25387  1cubrlem  25419  quart1  25434  log2cnv  25522  log2tlbnd  25523  log2ublem1  25524  log2ub  25527  emcllem1  25573  emcllem6  25578  basellem1  25658  basellem2  25659  basellem3  25660  basellem8  25665  ppiublem1  25778  ppiublem2  25779  ppiub  25780  chtublem  25787  chtub  25788  bcmono  25853  bclbnd  25856  bpos1lem  25858  bposlem1  25860  bposlem2  25861  bposlem3  25862  bposlem4  25863  bposlem5  25864  bposlem6  25865  bposlem7  25866  bposlem8  25867  bposlem9  25868  lgsdir2lem1  25901  1lgs  25916  gausslemma2dlem0c  25934  gausslemma2dlem0d  25935  gausslemma2dlem1a  25941  gausslemma2dlem2  25943  gausslemma2dlem3  25944  gausslemma2dlem5  25947  gausslemma2dlem6  25948  lgsquad2lem2  25961  2lgslem1a1  25965  2lgslem1a2  25966  2lgslem1c  25969  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgslem3  25980  2lgsoddprmlem1  25984  addsqrexnreu  26018  addsqnreup  26019  chebbnd1lem1  26045  chebbnd1lem3  26047  chebbnd1  26048  dchrisum0flblem2  26085  dchrisum0lem1  26092  mulog2sumlem2  26111  selberglem2  26122  chpdifbndlem1  26129  ercgrg  26303  axlowdimlem4  26731  axlowdimlem5  26732  axlowdimlem6  26733  axlowdimlem7  26734  axlowdimlem8  26735  axlowdimlem10  26737  axlowdimlem11  26738  graop  26814  grastruct  26815  uhgrunop  26860  upgrop  26879  upgrunop  26904  umgrunop  26906  usgrop  26948  usgr2v1e2w  27034  usgrexmpldifpr  27040  usgrexmpledg  27044  uhgrsubgrself  27062  uhgrspan1lem1  27082  upgrres1lem1  27091  fusgrfis  27112  vtxd0nedgb  27270  p1evtxdeqlem  27294  p1evtxdeq  27295  p1evtxdp1  27296  umgr2v2e  27307  vdegp1bi  27319  wlkcomp  27412  upgr2pthnlp  27513  usgr2trlncl  27541  usgr2pthlem  27544  clwlkcomp  27560  uspgrn2crct  27586  wwlksonvtx  27633  wspthnonp  27637  2wlkond  27716  2pthond  27721  2pthon3v  27722  umgr2adedgwlkonALT  27726  umgr2wlk  27728  umgr2wlkon  27729  wpthswwlks2on  27740  elwspths2spth  27746  0ewlk  27893  0pth  27904  0pthonv  27908  1pthon2v  27932  3wlkdlem4  27941  3trlond  27952  3pthond  27954  3spthond  27956  trlsegvdeglem3  28001  eupthvdres  28014  eupth2lemb  28016  ex-natded5.2i  28185  ex-an  28201  ex-id  28213  ex-po  28214  ex-fl  28226  ex-mod  28228  ex-exp  28229  ex-lcm  28237  nvz0  28445  ipidsq  28487  ipdirilem  28606  siilem1  28628  minvecolem2  28652  minvecolem3  28653  minvecolem4  28657  hvsubcan  28851  hvsubcan2  28852  normlem7tALT  28896  helch  29020  hsn0elch  29025  hhshsslem2  29045  hhsssh  29046  shscli  29094  shintcli  29106  shintcl  29107  chintcli  29108  chintcl  29109  shincli  29139  shsval2i  29164  omlsi  29181  chincli  29237  chabs1  29293  fh1i  29398  fh2i  29399  cm2ji  29402  pjnormi  29498  nmopsetn0  29642  nmfnsetn0  29655  lnophm  29796  nmcexi  29803  nmbdfnlb  29827  imaelshi  29835  nlelshi  29837  nmopadjlem  29866  nmopcoadji  29878  hmopidmch  29930  hmopidmpj  29931  sto1i  30013  stlei  30017  stji1i  30019  csmdsymi  30111  chirred  30172  cdj3lem1  30211  rpdp2cl  30558  dp2lt10  30560  dp2lt  30561  dp2ltc  30563  dpfrac1  30568  dplti  30581  dpgti  30582  dpexpp1  30584  dpadd3  30588  dpmul  30589  dpmul4  30590  xrsclat  30667  nn0archi  30916  lmatfvlem  31080  xrge0iifmhm  31182  qqh0  31225  qqh1  31226  rerrext  31250  cnrrext  31251  prsiga  31390  oms0  31555  coinfliprv  31740  ballotlem1  31744  ballotth  31795  signsw0g  31826  hgt750lemd  31919  hgt750lem  31922  hgt750lem2  31923  hgt750leme  31929  tgoldbachgt  31934  subfacval2  32434  erdszelem2  32439  cvmliftlem4  32535  satom  32603  satfv1  32610  sat1el2xp  32626  fmlaomn0  32637  satfdmfmla  32647  satfv1fvfmla1  32670  ex-sategoelelomsuc  32673  ex-sategoelel12  32674  prv0  32677  prv1n  32678  elmrsubrn  32767  msubfval  32771  problem4  32911  quad3  32913  dfpo2  32991  br6  32993  dfon2lem3  33030  poseq  33095  fullfunfnv  33407  fneref  33698  filnetlem2  33727  filnetlem3  33728  onpsstopbas  33778  dnizeq0  33814  dnibndlem12  33828  knoppcnlem5  33836  knoppcnlem8  33839  knoppcnlem10  33841  knoppcnlem11  33842  knoppndvlem14  33864  cnndvlem1  33876  bj-genr  33940  bj-genl  33941  bj-genan  33942  bj-2upln1upl  34339  bj-vtoclgfALT  34355  bj-brab2a1  34444  bj-opabssvv  34445  taupilem1  34605  topdifinf  34633  sin2h  34897  cos2h  34898  tan2h  34899  poimirlem1  34908  poimirlem2  34909  poimirlem3  34910  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem11  34918  poimirlem12  34919  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem29  34936  poimirlem31  34938  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  itg2addnclem2  34959  asindmre  34992  heiborlem7  35110  riscer  35281  refrelcoss3  35718  symrelcoss3  35720  ishlatiN  36506  0psubN  36900  atpsubN  36904  gcdcomnni  39117  gcdnegnni  39118  neggcdnni  39119  60gcd7e1  39126  lcmeprodgcdi  39128  lcm2un  39135  lcm3un  39136  mzpclall  39373  diophin  39418  diophun  39419  eldioph4b  39457  irrapx1  39474  2nn0ind  39591  aomclem4  39706  ifpid3g  39907  ifpid2g  39908  ifpbi1b  39918  eu0  39935  pwinfi  39972  rtrclex  40026  cnvrcl0  40034  dfrcl2  40068  relexp1idm  40108  relexp0idm  40109  clsk1independent  40445  lhe4.4ex1a  40710  expgrowth  40716  ax6e2nd  40941  uun0.1  41161  relopabVD  41284  ax6e2ndVD  41291  sb5ALTVD  41296  ax6e2ndALT  41313  dvmptconst  42248  dvmptidg  42250  dvmulcncf  42259  dvdivcncf  42261  dvnprodlem3  42282  itgsinexplem1  42288  volioof  42321  stoweidlem13  42347  stoweidlem14  42348  stoweidlem26  42360  stoweidlem34  42368  stoweidlem49  42383  stoweidlem59  42393  dirkertrigeqlem3  42434  dirkercncflem1  42437  dirkercncflem2  42438  fourierdlem57  42497  fourierdlem62  42502  fourierdlem103  42543  fourierdlem111  42551  fourierswlem  42564  fouriersw  42565  salexct2  42671  salexct3  42674  salgencntex  42675  salgensscntex  42676  gsumge0cl  42702  sge00  42707  sge0tsms  42711  0ome  42860  ovnlecvr  42889  ovn0lem  42896  hoidmvle  42931  ovnsubadd2lem  42976  smflimlem6  43101  mbfpsssmf  43108  smfmullem4  43118  smfpimbor1lem1  43122  astbstanbst  43194  aistbistaandb  43195  abnotataxb  43201  aifftbifffaibif  43206  confun4  43227  plcofph  43229  plvcofph  43231  plvcofphax  43232  plvofpos  43233  mdandyv0  43234  mdandyv1  43235  mdandyv2  43236  mdandyv3  43237  mdandyv4  43238  mdandyv5  43239  mdandyv6  43240  mdandyv7  43241  mdandyv8  43242  mdandyv9  43243  mdandyv10  43244  mdandyv11  43245  mdandyv12  43246  mdandyv13  43247  mdandyv14  43248  mdandyv15  43249  mdandyvr0  43250  mdandyvr1  43251  mdandyvr2  43252  mdandyvr3  43253  mdandyvr4  43254  mdandyvr5  43255  mdandyvr6  43256  mdandyvr7  43257  mdandyvrx0  43266  mdandyvrx1  43267  mdandyvrx2  43268  mdandyvrx3  43269  mdandyvrx4  43270  mdandyvrx5  43271  mdandyvrx6  43272  mdandyvrx7  43273  dandysum2p2e4  43283  or2expropbilem1  43316  dfnelbr2  43521  ich2exprop  43682  paireqne  43722  fmtno4prmfac  43783  31prm  43809  lighneallem4a  43822  41prothprmlem2  43832  zofldiv2ALTV  43876  nfermltl8rev  43956  nfermltl2rev  43957  nfermltlrev  43958  gbegt5  43975  gbowgt5  43976  gboge9  43978  9gbo  43988  11gbo  43989  nnsum3primes4  44002  nnsum3primesgbe  44006  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  tgblthelfgott  44029  tgoldbach  44031  isomgrref  44049  ushrisomgr  44055  nn0mnd  44135  mgmplusgiopALT  44150  sgrp2sgrp  44184  isrnghm  44212  2zrngaabl  44264  rnghmsscmap2  44293  rnghmsscmap  44294  funcrngcsetc  44318  funcrngcsetcALT  44319  rhmsscmap2  44339  rhmsscmap  44340  funcringcsetc  44355  funcringcsetcALTV2lem8  44363  funcringcsetclem8ALTV  44386  zlmodzxzlmod  44451  zlmodzxzel  44452  zlmodzxzscm  44454  zlmodzxzadd  44455  snlindsntorlem  44574  ldepspr  44577  lmod1lem2  44592  lmod1lem3  44593  lmod1lem4  44594  lmod1lem5  44595  lmodn0  44599  zlmodzxznm  44601  zlmodzxzldeplem  44602  zlmodzxzldeplem1  44604  zlmodzxzldeplem3  44606  lvecpsslmod  44611  ldepsnlinc  44612  ldepslinc  44613  expnegico01  44622  zofldiv2  44640  flnn0div2ge  44642  elbigo2  44661  nnlog2ge0lt1  44675  digfval  44706  dignnld  44712  dignn0flhalf  44727  prelrrx2  44749  eenglngeehlnmlem2  44774  rrxsphere  44784  line2  44788  line2x  44790  line2y  44791  itsclc0yqsollem2  44799  inlinecirc02plem  44822  alimp-surprise  44930  aacllem  44951