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  mzpclall  39344  diophin  39389  diophun  39390  eldioph4b  39428  irrapx1  39445  2nn0ind  39562  aomclem4  39677  ifpid3g  39878  ifpid2g  39879  ifpbi1b  39889  eu0  39906  pwinfi  39943  rtrclex  39997  cnvrcl0  40005  dfrcl2  40039  relexp1idm  40079  relexp0idm  40080  clsk1independent  40416  lhe4.4ex1a  40681  expgrowth  40687  ax6e2nd  40912  uun0.1  41132  relopabVD  41255  ax6e2ndVD  41262  sb5ALTVD  41267  ax6e2ndALT  41284  dvmptconst  42219  dvmptidg  42221  dvmulcncf  42230  dvdivcncf  42232  dvnprodlem3  42253  itgsinexplem1  42259  volioof  42292  stoweidlem13  42318  stoweidlem14  42319  stoweidlem26  42331  stoweidlem34  42339  stoweidlem49  42354  stoweidlem59  42364  dirkertrigeqlem3  42405  dirkercncflem1  42408  dirkercncflem2  42409  fourierdlem57  42468  fourierdlem62  42473  fourierdlem103  42514  fourierdlem111  42522  fourierswlem  42535  fouriersw  42536  salexct2  42642  salexct3  42645  salgencntex  42646  salgensscntex  42647  gsumge0cl  42673  sge00  42678  sge0tsms  42682  0ome  42831  ovnlecvr  42860  ovn0lem  42867  hoidmvle  42902  ovnsubadd2lem  42947  smflimlem6  43072  mbfpsssmf  43079  smfmullem4  43089  smfpimbor1lem1  43093  astbstanbst  43165  aistbistaandb  43166  abnotataxb  43172  aifftbifffaibif  43177  confun4  43198  plcofph  43200  plvcofph  43202  plvcofphax  43203  plvofpos  43204  mdandyv0  43205  mdandyv1  43206  mdandyv2  43207  mdandyv3  43208  mdandyv4  43209  mdandyv5  43210  mdandyv6  43211  mdandyv7  43212  mdandyv8  43213  mdandyv9  43214  mdandyv10  43215  mdandyv11  43216  mdandyv12  43217  mdandyv13  43218  mdandyv14  43219  mdandyv15  43220  mdandyvr0  43221  mdandyvr1  43222  mdandyvr2  43223  mdandyvr3  43224  mdandyvr4  43225  mdandyvr5  43226  mdandyvr6  43227  mdandyvr7  43228  mdandyvrx0  43237  mdandyvrx1  43238  mdandyvrx2  43239  mdandyvrx3  43240  mdandyvrx4  43241  mdandyvrx5  43242  mdandyvrx6  43243  mdandyvrx7  43244  dandysum2p2e4  43254  or2expropbilem1  43287  dfnelbr2  43492  ich2exprop  43653  paireqne  43693  fmtno4prmfac  43754  31prm  43780  lighneallem4a  43793  41prothprmlem2  43803  zofldiv2ALTV  43847  nfermltl8rev  43927  nfermltl2rev  43928  nfermltlrev  43929  gbegt5  43946  gbowgt5  43947  gboge9  43949  9gbo  43959  11gbo  43960  nnsum3primes4  43973  nnsum3primesgbe  43977  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  tgblthelfgott  44000  tgoldbach  44002  isomgrref  44020  ushrisomgr  44026  nn0mnd  44106  mgmplusgiopALT  44121  sgrp2sgrp  44155  isrnghm  44183  2zrngaabl  44235  rnghmsscmap2  44264  rnghmsscmap  44265  funcrngcsetc  44289  funcrngcsetcALT  44290  rhmsscmap2  44310  rhmsscmap  44311  funcringcsetc  44326  funcringcsetcALTV2lem8  44334  funcringcsetclem8ALTV  44357  zlmodzxzlmod  44422  zlmodzxzel  44423  zlmodzxzscm  44425  zlmodzxzadd  44426  snlindsntorlem  44545  ldepspr  44548  lmod1lem2  44563  lmod1lem3  44564  lmod1lem4  44565  lmod1lem5  44566  lmodn0  44570  zlmodzxznm  44572  zlmodzxzldeplem  44573  zlmodzxzldeplem1  44575  zlmodzxzldeplem3  44577  lvecpsslmod  44582  ldepsnlinc  44583  ldepslinc  44584  expnegico01  44593  zofldiv2  44611  flnn0div2ge  44613  elbigo2  44632  nnlog2ge0lt1  44646  digfval  44677  dignnld  44683  dignn0flhalf  44698  prelrrx2  44720  eenglngeehlnmlem2  44745  rrxsphere  44755  line2  44759  line2x  44761  line2y  44762  itsclc0yqsollem2  44770  inlinecirc02plem  44793  alimp-surprise  44901  aacllem  44922