Theorem pm3.2i 472

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

Syntax hints:   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  mp4an  692  pm4.87  842  3pm3.2i  1340  unssi  4186  ssini  4232  opthhausdorff  5518  elvv  5751  elopaelxp  5766  relopabiv  5821  relopabi  5823  dfpo2  6296  funpr  6605  funcnvpr  6611  mpov  7520  caovcom  7604  snnex  7745  pwnex  7746  1st2val  8003  2nd2val  8004  elxp7  8010  opreuopreu  8020  mptmpoopabbrdOLD  8069  poxp2  8129  poseq  8144  wfrlem13OLD  8321  wfr3OLD  8338  tfr1a  8394  oeoa  8597  oeoe  8599  erov  8808  endisj  9058  phplem2OLD  9218  snopfsupp  9386  ssttrcl  9710  ttrclselem2  9721  r1funlim  9761  dfac2b  10125  cflecard  10248  canth4  10642  canthnumlem  10643  canthwelem  10645  canthp1lem2  10648  pwfseqlem4  10657  wunex3  10736  addsrpr  11070  mulsrpr  11071  recexsrlem  11098  mulcani  11853  div1  11903  recdiv  11920  divdiv1  11925  divdiv2  11926  div23i  11972  div11i  11973  divmuldivi  11974  divadddivi  11976  divdivdivi  11977  lemulge11  12076  negiso  12194  dfnn3  12226  2cnne0  12422  2rene0  12423  halfpm6th  12433  avglt1  12450  avglt2  12451  div4p1lem1div2  12467  3halfnz  12641  divlt1lt  13043  divle1le  13044  nnledivrp  13086  x2times  13278  xrsupsslem  13286  xrinfmsslem  13287  fz0to4untppr  13604  om2uzoi  13920  fzennn  13933  expge1  14065  sqoddm1div8  14206  faclbnd2  14251  faclbnd4lem1  14253  4bc2eq6  14289  hashfxnn0  14297  hashsnlei  14378  hashunlei  14385  hashsslei  14386  hash2prb  14433  repswccat  14736  cshwsexaOLD  14775  funcnvs4  14866  f1oun2prg  14868  wrdlen2i  14893  relexpaddg  15000  cjreb  15070  sqrt2gt1lt2  15221  abs1m  15282  bpoly3  16002  ege2le3  16033  efi4p  16080  efival  16095  sin01bnd  16128  cos01bnd  16129  cos1bnd  16130  cos2bnd  16131  sin01gt0  16133  cos01gt0  16134  sin02gt0  16135  sincos2sgn  16137  sin4lt0  16138  egt2lt3  16149  rpnnen2lem3  16159  rpnnen2lem11  16167  nthruc  16195  nthruz  16196  3dvdsdec  16275  3dvds2dec  16276  mod2eq1n2dvds  16290  halfleoddlt  16305  divalglem5  16340  ndvdsi  16355  flodddiv4  16356  flodddiv4lt  16358  bitsp1o  16374  3lcm2e6woprm  16552  6lcm4e12  16553  pcrec  16791  prmrec  16855  prmgaplcmlem1  16984  prmgaplcm  16993  modsubi  17005  structfn  17089  strleun  17090  slotsdifipndx  17280  slotsdifplendx  17320  slotsdifdsndx  17339  slotsdifunifndx  17346  slotsdifplendx2  17362  slotsdifocndx  17363  isofn  17722  sscres  17770  funcestrcsetclem7  18098  funcestrcsetclem8  18099  fullestrcsetc  18103  mgmnsgrpex  18812  pwmnd  18818  ga0  19162  symg2bas  19260  f1otrspeq  19315  psgnsn  19388  0frgp  19647  gsummptnn0fz  19854  srgbinomlem4  20052  cnfldfun  20956  cnfldfunALT  20957  cnfldfunALTOLD  20958  cnfld1  20970  cnsubdrglem  20996  expmhm  21014  expghm  21045  psrbag0  21623  psrbagsn  21624  coe1fsupp  21738  coe1mul2  21791  evls1sca  21842  matmulr  21940  mat1dimelbas  21973  mat1f1o  21980  m2detleib  22133  smadiadetglem1  22173  pmatcollpw3fi1lem2  22289  cpmidpmatlem2  22373  cpmadumatpolylem1  22383  cayhamlem3  22389  cayhamlem4  22390  isbasis3g  22452  fctop  22507  cctop  22509  refref  23017  bl2in  23906  dscmet  24081  iihalf1  24447  iihalf2  24449  icopnfhmeo  24459  iccpnfhmeo  24461  xrhmeo  24462  iscvsi  24645  zclmncvs  24665  ncvs1  24674  ehl2eudis  24939  minveclem2  24943  minveclem4  24949  ovolunlem1a  25013  volf  25046  i1f1lem  25206  mbfi1fseqlem5  25237  dveflem  25496  pilem2  25964  pilem3  25965  sinhalfpilem  25973  sincosq1lem  26007  tangtx  26015  sinq12gt0  26017  sincos4thpi  26023  sincos6thpi  26025  sincos3rdpi  26026  pigt3  26027  pige3ALT  26029  coseq1  26034  efeq1  26037  efif1olem4  26054  angneg  26308  ang180lem1  26314  1cubrlem  26346  quart1  26361  log2cnv  26449  log2tlbnd  26450  log2ublem1  26451  log2ub  26454  emcllem1  26500  emcllem6  26505  basellem1  26585  basellem2  26586  basellem3  26587  basellem8  26592  ppiublem1  26705  ppiublem2  26706  ppiub  26707  chtublem  26714  chtub  26715  bcmono  26780  bclbnd  26783  bpos1lem  26785  bposlem1  26787  bposlem2  26788  bposlem3  26789  bposlem4  26790  bposlem5  26791  bposlem6  26792  bposlem7  26793  bposlem8  26794  bposlem9  26795  lgsdir2lem1  26828  1lgs  26843  gausslemma2dlem0c  26861  gausslemma2dlem0d  26862  gausslemma2dlem1a  26868  gausslemma2dlem2  26870  gausslemma2dlem3  26871  gausslemma2dlem5  26874  gausslemma2dlem6  26875  lgsquad2lem2  26888  2lgslem1a1  26892  2lgslem1a2  26893  2lgslem1c  26896  2lgslem3a  26899  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  2lgslem3  26907  2lgsoddprmlem1  26911  addsqrexnreu  26945  addsqnreup  26946  chebbnd1lem1  26972  chebbnd1lem3  26974  chebbnd1  26975  dchrisum0flblem2  27012  dchrisum0lem1  27019  mulog2sumlem2  27038  selberglem2  27049  chpdifbndlem1  27056  mulscl  27593  sltmul  27595  divs1  27654  precsexlem8  27663  slotsinbpsd  27723  slotslnbpsd  27724  ercgrg  27799  axlowdimlem4  28234  axlowdimlem5  28235  axlowdimlem6  28236  axlowdimlem7  28237  axlowdimlem8  28238  axlowdimlem10  28240  axlowdimlem11  28241  graop  28320  grastruct  28321  uhgrunop  28366  upgrop  28385  upgrunop  28410  umgrunop  28412  usgrop  28454  usgr2v1e2w  28540  usgrexmpldifpr  28546  usgrexmpledg  28550  uhgrsubgrself  28568  uhgrspan1lem1  28588  upgrres1lem1  28597  fusgrfis  28618  vtxd0nedgb  28776  p1evtxdeqlem  28800  p1evtxdeq  28801  p1evtxdp1  28802  umgr2v2e  28813  vdegp1bi  28825  wlkcomp  28919  upgr2pthnlp  29020  usgr2trlncl  29048  usgr2pthlem  29051  clwlkcomp  29067  uspgrn2crct  29093  wwlksonvtx  29140  wspthnonp  29144  2wlkond  29222  2pthond  29227  2pthon3v  29228  umgr2adedgwlkonALT  29232  umgr2wlk  29234  umgr2wlkon  29235  wpthswwlks2on  29246  elwspths2spth  29252  0ewlk  29398  0pth  29409  0pthonv  29413  1pthon2v  29437  3wlkdlem4  29446  3trlond  29457  3pthond  29459  3spthond  29461  trlsegvdeglem3  29506  eupthvdres  29519  eupth2lemb  29521  ex-natded5.2i  29690  ex-an  29706  ex-id  29718  ex-po  29719  ex-fl  29731  ex-mod  29733  ex-exp  29734  ex-lcm  29742  nvz0  29952  ipidsq  29994  ipdirilem  30113  siilem1  30135  minvecolem2  30159  minvecolem3  30160  minvecolem4  30164  hvsubcan  30358  hvsubcan2  30359  normlem7tALT  30403  helch  30527  hsn0elch  30532  hhshsslem2  30552  hhsssh  30553  shscli  30601  shintcli  30613  shintcl  30614  chintcli  30615  chintcl  30616  shincli  30646  shsval2i  30671  omlsi  30688  chincli  30744  chabs1  30800  fh1i  30905  fh2i  30906  cm2ji  30909  pjnormi  31005  nmopsetn0  31149  nmfnsetn0  31162  lnophm  31303  nmcexi  31310  nmbdfnlb  31334  imaelshi  31342  nlelshi  31344  nmopadjlem  31373  nmopcoadji  31385  hmopidmch  31437  hmopidmpj  31438  sto1i  31520  stlei  31524  stji1i  31526  csmdsymi  31618  chirred  31679  cdj3lem1  31718  rpdp2cl  32079  dp2lt10  32081  dp2lt  32082  dp2ltc  32084  dpfrac1  32089  dplti  32102  dpgti  32103  dpexpp1  32105  dpadd3  32109  dpmul  32110  dpmul4  32111  xrsclat  32212  nn0archi  32493  lmatfvlem  32826  xrge0iifmhm  32950  qqh0  32995  qqh1  32996  rerrext  33020  cnrrext  33021  prsiga  33160  oms0  33327  coinfliprv  33512  ballotlem1  33516  ballotth  33567  signsw0g  33598  hgt750lemd  33691  hgt750lem  33694  hgt750lem2  33695  hgt750leme  33701  tgoldbachgt  33706  subfacval2  34209  erdszelem2  34214  cvmliftlem4  34310  satom  34378  satfv1  34385  sat1el2xp  34401  fmlaomn0  34412  satfdmfmla  34422  satfv1fvfmla1  34445  ex-sategoelelomsuc  34448  ex-sategoelel12  34449  prv0  34452  prv1n  34453  elmrsubrn  34542  msubfval  34546  problem4  34684  quad3  34686  br6  34758  dfon2lem3  34788  fullfunfnv  34949  gg-cnfldfun  35228  gg-cnfldfunALT  35229  gg-cnfld1  35232  fneref  35283  filnetlem2  35312  filnetlem3  35313  onpsstopbas  35363  dnizeq0  35399  dnibndlem12  35413  knoppcnlem5  35421  knoppcnlem8  35424  knoppcnlem10  35426  knoppcnlem11  35427  knoppndvlem14  35449  cnndvlem1  35461  bj-genr  35532  bj-genl  35533  bj-genan  35534  bj-2upln1upl  35953  bj-vtoclgfALT  35988  bj-brab2a1  36078  bj-opabssvv  36079  taupilem1  36250  topdifinf  36278  sin2h  36526  cos2h  36527  tan2h  36528  poimirlem1  36537  poimirlem2  36538  poimirlem3  36539  poimirlem4  36540  poimirlem6  36542  poimirlem7  36543  poimirlem11  36547  poimirlem12  36548  poimirlem16  36552  poimirlem17  36553  poimirlem19  36555  poimirlem20  36556  poimirlem22  36558  poimirlem23  36559  poimirlem24  36560  poimirlem25  36561  poimirlem26  36562  poimirlem29  36565  poimirlem31  36567  mblfinlem3  36575  mblfinlem4  36576  ismblfin  36577  itg2addnclem2  36588  asindmre  36619  heiborlem7  36733  riscer  36904  refrelcoss3  37381  symrelcoss3  37383  ishlatiN  38273  0psubN  38668  atpsubN  38672  gcdcomnni  40902  gcdnegnni  40903  neggcdnni  40904  60gcd7e1  40918  lcmeprodgcdi  40920  lcm2un  40927  lcm3un  40928  lcmineqlem4  40945  lcmineqlem6  40947  3lexlogpow5ineq1  40967  aks4d1p1p2  40983  mzpclall  41513  diophin  41558  diophun  41559  eldioph4b  41597  irrapx1  41614  2nn0ind  41732  aomclem4  41847  onexlimgt  42040  nnoeomeqom  42110  oaomoencom  42115  oenassex  42116  succlg  42126  dflim5  42127  omabs2  42130  tfsconcatfv2  42138  ifpid3g  42291  ifpid2g  42292  ifpbi1b  42302  eu0  42319  pwinfi  42363  rtrclex  42416  cnvrcl0  42424  dfrcl2  42473  relexp1idm  42513  relexp0idm  42514  clsk1independent  42845  lhe4.4ex1a  43136  expgrowth  43142  ax6e2nd  43367  uun0.1  43587  relopabVD  43710  ax6e2ndVD  43717  sb5ALTVD  43722  ax6e2ndALT  43739  rexanuz2nf  44251  dvmptconst  44679  dvmptidg  44681  dvmulcncf  44689  dvdivcncf  44691  dvnprodlem3  44712  itgsinexplem1  44718  volioof  44751  stoweidlem13  44777  stoweidlem14  44778  stoweidlem26  44790  stoweidlem34  44798  stoweidlem49  44813  stoweidlem59  44823  dirkertrigeqlem3  44864  dirkercncflem1  44867  dirkercncflem2  44868  fourierdlem57  44927  fourierdlem62  44932  fourierdlem103  44973  fourierdlem111  44981  fourierswlem  44994  fouriersw  44995  salexct2  45103  salexct3  45106  salgencntex  45107  salgensscntex  45108  gsumge0cl  45135  sge00  45140  sge0tsms  45144  0ome  45293  ovnlecvr  45322  ovn0lem  45329  hoidmvle  45364  ovnsubadd2lem  45409  smflimlem6  45540  mbfpsssmf  45547  smfmullem4  45558  smfpimbor1lem1  45562  astbstanbst  45667  aistbistaandb  45668  abnotataxb  45674  aifftbifffaibif  45679  confun4  45700  plcofph  45702  plvcofph  45704  plvcofphax  45705  plvofpos  45706  mdandyv0  45707  mdandyv1  45708  mdandyv2  45709  mdandyv3  45710  mdandyv4  45711  mdandyv5  45712  mdandyv6  45713  mdandyv7  45714  mdandyv8  45715  mdandyv9  45716  mdandyv10  45717  mdandyv11  45718  mdandyv12  45719  mdandyv13  45720  mdandyv14  45721  mdandyv15  45722  mdandyvr0  45723  mdandyvr1  45724  mdandyvr2  45725  mdandyvr3  45726  mdandyvr4  45727  mdandyvr5  45728  mdandyvr6  45729  mdandyvr7  45730  mdandyvrx0  45739  mdandyvrx1  45740  mdandyvrx2  45741  mdandyvrx3  45742  mdandyvrx4  45743  mdandyvrx5  45744  mdandyvrx6  45745  mdandyvrx7  45746  dandysum2p2e4  45756  or2expropbilem1  45790  dfnelbr2  46029  ich2exprop  46187  paireqne  46227  fmtno4prmfac  46288  31prm  46313  lighneallem4a  46324  41prothprmlem2  46334  zofldiv2ALTV  46378  nfermltl8rev  46458  nfermltl2rev  46459  nfermltlrev  46460  gbegt5  46477  gbowgt5  46478  gboge9  46480  9gbo  46490  11gbo  46491  nnsum3primes4  46504  nnsum3primesgbe  46508  nnsum4primesodd  46512  nnsum4primesoddALTV  46513  nnsum4primeseven  46516  nnsum4primesevenALTV  46517  tgblthelfgott  46531  tgoldbach  46533  isomgrref  46551  ushrisomgr  46557  nn0mnd  46637  mgmplusgiopALT  46652  sgrp2sgrp  46686  isrnghm  46738  pzriprnglem4  46856  pzriprnglem9  46861  pzriprnglem14  46866  pzriprng1ALT  46868  2zrngaabl  46890  rnghmsscmap2  46919  rnghmsscmap  46920  funcrngcsetc  46944  funcrngcsetcALT  46945  rhmsscmap2  46965  rhmsscmap  46966  funcringcsetc  46981  funcringcsetcALTV2lem8  46989  funcringcsetclem8ALTV  47012  zlmodzxzlmod  47078  zlmodzxzel  47079  zlmodzxzscm  47081  zlmodzxzadd  47082  snlindsntorlem  47199  ldepspr  47202  lmod1lem2  47217  lmod1lem3  47218  lmod1lem4  47219  lmod1lem5  47220  lmodn0  47224  zlmodzxznm  47226  zlmodzxzldeplem  47227  zlmodzxzldeplem1  47229  zlmodzxzldeplem3  47231  lvecpsslmod  47236  ldepsnlinc  47237  ldepslinc  47238  expnegico01  47247  zofldiv2  47265  flnn0div2ge  47267  elbigo2  47286  nnlog2ge0lt1  47300  digfval  47331  dignnld  47337  dignn0flhalf  47352  2arymaptfo  47388  itcovalt2lem1  47409  prelrrx2  47447  eenglngeehlnmlem2  47472  rrxsphere  47482  line2  47486  line2x  47488  line2y  47489  itsclc0yqsollem2  47497  inlinecirc02plem  47520  sepfsepc  47608  alimp-surprise  47875  aacllem  47896