Theorem 3adant2 1132

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3adant2	⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)

Proof of Theorem 3adant2

Step	Hyp	Ref	Expression
1		3adant.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 716	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	3impa 1110	1 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3ad2ant1  1134  3simpb  1150  3imp3i2an  1347  eupickb  2635  eqeu  3652  onunel  6430  iotan0  6488  funopg  6532  dff1o2  6785  fvelimad  6907  unima  6915  fnimapr  6923  fvmptt  6968  fnreseql  7000  xpprsng  7093  f1elima  7218  f1ounsn  7227  f13dfv  7229  f1ocnvfvb  7234  f1cdmsn  7237  f1ofvswap  7261  oprssov  7536  resf1extb  7885  resf1ext2b  7886  funelss  8000  poxp  8078  poxp2  8093  poxp3  8100  smoiso  8302  oaord  8482  oaword  8484  omcan  8504  omwordri  8507  odi  8514  omeulem1  8517  oeord  8524  oecan  8525  oewordri  8528  oeordsuc  8530  nnaord  8555  nnaordr  8556  nndi  8559  nnaword  8563  nnmwordri  8572  naddel2  8624  naddss1  8625  naddss2  8626  erov  8761  ecopovtrn  8767  mapsnd  8834  f1dom3g  8914  xpdom3  9013  mapxpen  9081  dif1en  9096  findcard  9098  f1domfi2  9116  entrfir  9125  domtrfil  9126  domtrfir  9128  sbthfilem  9132  sdomdomtrfi  9135  php3  9143  findcard3  9193  indexfi  9270  suppr  9385  infpr  9418  r111  9699  tcrank  9808  acndom  9973  infdif2  10131  infxpdom  10132  cfeq0  10178  cfsuc  10179  cfflb  10181  cflim2  10185  cfsmolem  10192  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  pwcfsdom  10506  tsktrss  10684  tsksuc  10685  tskuni  10706  adderpqlem  10877  mulerpqlem  10878  mulcanenq  10883  distrnq  10884  ltsonq  10892  ltanq  10894  ltmnq  10895  distrlem1pr  10948  distrlem5pr  10950  ltsopr  10955  ltsosr  11017  ltasr  11023  adddir  11135  axlttrn  11218  letr  11240  nnncan1  11430  npncan3  11432  pnpcan2  11434  subdi  11583  subdir  11584  mulcan1g  11803  mulcan2g  11804  divmul  11812  div23  11828  div13  11830  muldivdir  11847  divsubdir  11848  subdivcomb1  11850  divcan7  11864  ltmul2  12006  lemul1  12007  lemul2  12008  lemul2a  12010  lediv1  12021  ltmuldiv2  12030  lemuldiv  12036  lemuldiv2  12037  ltdiv2  12042  lediv2  12046  infrelb  12141  nndivtr  12224  bndndx  12436  nn0n0n1ge2  12505  fnn0ind  12628  addlelt  13058  xrletr  13109  qsqueeze  13153  xleadd2a  13206  xleadd1  13207  xltadd2  13209  xltmul2  13245  supxrbnd  13280  iooneg  13424  iccneg  13425  icoshft  13426  icoshftf1o  13427  zltaddlt1le  13458  fzen  13495  uzsubsubfz  13500  ssfzunsnext  13523  fzrevral2  13567  fzshftral  13569  fz0fzdiffz0  13591  elfzmlbp  13593  elfzo  13615  nelfzo  13619  fzoaddel2  13675  fzosubel2  13680  ssfzo12bi  13716  fzonfzoufzol  13726  subfzo0  13747  flltdivnn0lt  13792  modmulnn  13848  modcyc  13865  modaddabs  13870  modaddmod  13871  modmuladd  13875  modadd2mod  13883  modsubmod  13891  modsubmodmod  13892  modaddmodup  13896  modmulmod  13898  modsubdir  13902  modfzo0difsn  13905  modsumfzodifsn  13906  uzindi  13944  axdc4uzlem  13945  expneg2  14032  expdiv  14075  expubnd  14140  mulbinom2  14185  bernneq2  14192  expnngt1  14203  hashinfxadd  14347  hashunsngx  14355  hashunsnggt  14356  hashfundm  14404  hashf1dmcdm  14406  hashdifsnp1  14468  ccatval3  14541  ccatfv0  14546  ccatval1lsw  14547  ccats1val2  14590  ccatw2s1p1  14599  swrdnd  14617  pfxsuffeqwrdeq  14660  pfxsuff1eqwrdeq  14661  swrdswrd  14667  pfxpfx  14670  wrd2ind  14685  swrdccatin1  14687  pfxccatin12lem1  14690  swrdccatin2  14691  pfxccatin12lem3  14694  swrdccat  14697  pfxccatpfx1  14698  pfxccatpfx2  14699  swrdccat3blem  14701  repswswrd  14746  repswpfx  14747  repswccat  14748  cshwidxmod  14765  2cshw  14775  3cshw  14780  scshwfzeqfzo  14788  cshwcsh2id  14790  cshimadifsn  14791  cshimadifsn0  14792  ccatco  14797  cshco  14798  swrdco  14799  pfxco  14800  lswco  14801  swrds2  14902  2swrd2eqwrdeq  14915  shftuz  15031  abs3dif  15294  fsumdifsnconst  15754  modfsummods  15756  sin02gt0  16159  dvdsval2  16224  dvdscmul  16251  dvdsmulc  16252  dvdscmulr  16253  dvdsmulcr  16254  divalglem8  16369  ndvdssub  16378  dvdsexpim  16524  rpmulgcd  16526  expgcd  16532  zexpgcd  16534  coprmprod  16630  cncongr1  16636  cncongr2  16637  isprm3  16652  modprm0  16776  coprimeprodsq  16779  pythagtriplem12  16797  pythagtriplem14  16799  pcprendvds  16811  pcmul  16822  pcdiv  16823  pcqcl  16827  pcqdiv  16828  pcdvdsb  16840  vdwnnlem1  16966  hashbcss  16975  cshwshashlem1  17066  fvsetsid  17138  setsstruct2  17144  setsstruct  17146  mrcss  17582  mrcsscl  17586  mrcun  17588  cofulid  17857  catcisolem  18077  funcsetcestrclem9  18129  latleeqj1  18417  lubun  18481  clatleglb  18484  pslem  18538  dirtr  18568  mgmb1mgm1  18623  pwspjmhm  18798  grpinvid1  18967  grpinvid2  18968  grpasscan1  18977  grpasscan2  18978  grpinvadd  18994  grpsubf  18995  grpsubrcan  18997  grpinvsub  18998  grpsubeq0  19002  grpsubadd0sub  19003  grppncan  19007  grpnpcan  19008  mulgnn0p1  19061  mulgaddcomlem  19073  mulginvcom  19075  mulginvinv  19076  subgsubcl  19113  subgsub  19114  eqglact  19154  qussub  19166  ghmsub  19199  psgnunilem4  19472  oddvds2  19541  odsubdvds  19546  gexnnod  19563  slwn0  19590  dvrcl  20384  unitdvcl  20385  dvrcan1  20389  dvrcan3  20390  dvreq1  20391  rngisom1  20446  rngisomring  20447  subrgdv  20566  abvsubtri  20804  idsrngd  20833  lmodvsubval2  20912  lsmcl  21078  lsmsp2  21082  lspsntrim  21093  rngqiprngimfolem  21288  lidldvgen  21332  cncrng  21373  chrcong  21507  dvdschrmulg  21508  zndvds  21529  zntoslem  21536  ocvsscon  21655  obselocv  21708  frlmphl  21761  ascldimul  21868  mpfsubrg  22089  ply1tmcl  22237  eqcoe1ply1eq  22264  gsummoncoe1  22273  lply1binomsc  22276  mamudm  22360  mamufacex  22361  scmatf1  22496  scmatf1o  22497  scmatrngiso  22501  submabas  22543  mdetdiaglem  22563  mdetralt2  22574  mdetero  22575  mdetunilem2  22578  mdetunilem6  22582  m2detleiblem7  22592  maducoeval2  22605  gsummatr01lem3  22622  gsummatr01  22624  smadiadetglem2  22637  cramerlem1  22652  mply1topmatcl  22770  mp2pm2mplem4  22774  ntrin  23026  elnei  23076  neindisj2  23088  ordtopn3  23161  leordtval2  23177  lecldbas  23184  cnrest2  23251  cmpsublem  23364  ptrescn  23604  xkococn  23625  kqfeq  23689  snfbas  23831  neifil  23845  fclsrest  23989  utopsnnei  24214  neipcfilu  24260  psmetsym  24275  psmetge0  24277  xmetge0  24309  xmetsym  24312  metustto  24518  metustbl  24531  restmetu  24535  nm2dif  24590  nmtri  24591  cnmet  24736  cnmpopc  24895  iihalf1  24898  iihalf2  24900  iocopnst  24907  clmnegsubdi2  25072  clmsub4  25073  clmvsubval2  25077  ncvspi  25123  cphsqrtcl3  25154  cph2ass  25180  cphipval2  25208  cphipval  25210  caublcls  25276  bcthlem3  25293  bcthlem4  25294  srabn  25327  cssbn  25342  cmslsschl  25344  rrxmet  25375  rrxdsfi  25378  iblconst  25785  dvdsq1p  26128  coeid3  26205  aannenlem2  26295  pserdvlem2  26393  tanord1  26501  cxpef  26629  recxpcl  26639  logbchbase  26735  relogbcl  26737  relogbzcl  26738  logbleb  26747  logblt  26748  relogbcxpb  26751  lawcos  26780  pythag  26781  isosctrlem1  26782  isosctrlem2  26783  lgsmodeq  27305  lgsmulsqcoprm  27306  gausslemma2dlem1a  27328  2lgsoddprmlem2  27372  ltsres  27626  lestr  27726  cofcutr  27916  lrrecpo  27933  ltadds2im  27978  leadds2im  27980  leadds1  27981  leadds2  27982  ltadds1  27984  addscan2  27985  addscan1  27986  ltsubs1  28068  divmulsw  28185  oldfib  28369  zsoring  28401  bdayfinbndlem1  28459  ax5seglem1  28997  axcontlem2  29034  axcontlem8  29040  upgrpredgv  29208  numedglnl  29213  issubgr2  29341  uhgrissubgr  29344  egrsubgr  29346  nbusgrfi  29443  nb3grprlem2  29450  cplgr3v  29504  cusgrsizeindslem  29520  finsumvtxdg2size  29619  rusgrpropadjvtx  29654  upgrwlkvtxedg  29713  usgr2trlncl  29828  uspgrn2crct  29876  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  wwlksnextproplem3  29979  umgr2adedgwlklem  30012  rusgr0edg  30044  clwwlk1loop  30058  clwwlkccatlem  30059  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwwisshclwwslemlem  30083  erclwwlktr  30092  clwwlkel  30116  erclwwlkntr  30141  clwwlknonex2lem2  30178  uhgr3cyclex  30252  umgr3cyclex  30253  eucrctshift  30313  frgr3v  30345  3cyclfrgrrn  30356  frgrwopreglem5a  30381  frgr2wsp1  30400  extwwlkfab  30422  clwwlknonclwlknonf1o  30432  numclwwlk3lem1  30452  numclwwlk5  30458  numclwwlk6  30460  isgrpo  30568  grpoinvid1  30599  grpoinvid2  30600  grpoinvop  30604  grpodivinv  30607  grpoinvdiv  30608  grpodivf  30609  grponpcan  30614  ablonncan  30627  nvmval  30713  nvmval2  30714  nvmfval  30715  nvmul0or  30721  nvpncan2  30724  nvaddsub4  30728  nvmeq0  30729  nvdif  30737  nvpi  30738  nvmtri  30742  nvabs  30743  imsmetlem  30761  ipval2lem3  30776  ipval2  30778  4ipval2  30779  ipval3  30780  nmooge0  30838  blometi  30874  hvaddsub12  31109  hvsubdistr1  31120  hvsubdistr2  31121  hvaddcan2  31142  hvmulcan  31143  hvmulcan2  31144  hvsubcan  31145  hvsubcan2  31146  his7  31161  his2sub  31163  his2sub2  31164  norm3dif2  31222  shsubcl  31291  hhssnv  31335  shlej2  31432  fh2  31690  cm2j  31691  pjoi0  31788  hodcl  31818  hosubdi  31879  unopf1o  31987  unopadj  31990  adj2  32005  braadd  32016  bramul  32017  lnopaddmuli  32044  lnopsubmuli  32046  homco2  32048  lnfnaddmuli  32116  adjlnop  32157  leopmul  32205  leoptr  32208  pjimai  32247  atcv1  32451  atexch  32452  atcvatlem  32456  fcoinvbr  32675  preiman0  32783  divnumden2  32889  sgn3da  32907  xdivmul  32984  cshf1o  33022  resvsca  33392  idlsrgcmnd  33575  hasheuni  34229  difelsiga  34277  cndprobin  34578  bayesth  34583  signstfvp  34715  breprexplemc  34776  trssfir1om  35255  fineqvac  35260  fineqvnttrclselem1  35265  fineqvnttrclselem3  35267  trssfir1omregs  35280  swrdrevpfx  35299  swrdwlk  35309  lediv2aALT  35859  fununiq  35951  dfrdg2  35975  clsun  36510  neiin  36514  rdgeqoa  37686  curfv  37921  matunitlindflem1  37937  poimirlem32  37973  ftc1anclem4  38017  areacirc  38034  filbcmb  38061  ismtybnd  38128  grpoeqdivid  38202  ghomco  38212  rngonegrmul  38265  zerdivemp1x  38268  rngohomco  38295  rngoisoco  38303  riscer  38309  intidl  38350  isfldidl  38389  eceldmqsxrncnvepres  38757  eceldmqsxrncnvepres2  38758  brredunds  39031  lshpnelb  39430  opnlen0  39634  opcon3b  39642  opcon2b  39643  oplecon3b  39646  opltcon3b  39650  opltcon2b  39652  oldmm1  39663  oldmm4  39666  oldmj1  39667  oldmj4  39670  cvrval2  39720  cvrcon3b  39723  leatb  39738  atcmp  39757  atcvreq0  39760  atlatle  39766  athgt  39902  3dim2  39914  islln2a  39963  lplnnleat  39988  lvolnleat  40029  4atlem10  40052  4atlem11  40055  4atlem12  40058  dalem21  40140  dalem22  40141  dalem23  40142  dalem29  40147  dalem30  40148  dalem31N  40149  dalem32  40150  dalem33  40151  dalem34  40152  dalem35  40153  dalem36  40154  dalem37  40155  dalem40  40158  dalem46  40164  dalem47  40165  dalem51  40169  dalem52  40170  dalem58  40176  dalem59  40177  pmaple  40207  paddclN  40288  pmapjoin  40298  pmapjat1  40299  elpcliN  40339  pclssN  40340  pclun2N  40345  2polcon4bN  40364  paddunN  40373  poldmj1N  40374  pmapj2N  40375  pmapocjN  40376  psubclinN  40394  paddatclN  40395  poml4N  40399  lautco  40543  ldilco  40562  ltrneq2  40594  trljat1  40612  cdlemc1  40637  cdleme10  40700  ltrnco  41165  trlcocnv  41166  trljco  41186  trljco2  41187  cdlemi1  41264  tendocnv  41467  diaord  41493  dibord  41605  dihord3  41703  dihord4  41704  dihmeetlem2N  41745  dihmeetlem4preN  41752  dochdmj1  41836  hdmap10lem  42285  lcmineqlem1  42468  sticksstones2  42586  readdsub  42816  reltsub1  42818  renpncan3  42823  reppncan  42825  resubdi  42828  readdcan2  42845  mzprename  43181  dvdsrabdioph  43238  pell14qrdivcl  43293  monotoddzz  43371  jm2.19lem2  43418  jm2.19  43421  relexpaddss  44145  k0004lem3  44576  dvconstbi  44761  chordthmALT  45359  isosctrlem1ALT  45360  ssinc  45517  ssdec  45518  wessf1ornlem  45615  disjf1o  45621  ssnnf1octb  45624  projf1o  45626  mapssbi  45642  iunmapsn  45646  upbdrech  45738  iuneqfzuzlem  45764  suplesup  45769  rexabslelem  45846  climxrrelem  46177  limsupresxr  46194  liminfresxr  46195  liminfvalxr  46211  xlimliminflimsup  46290  cncfshift  46302  cncfperiod  46307  cncfuni  46314  icccncfext  46315  dvmptfprodlem  46372  dvnprodlem1  46374  itgspltprt  46407  ismbl3  46414  stoweidlem3  46431  stoweidlem10  46438  stoweidlem19  46447  stoweidlem31  46459  stoweidlem34  46462  stoweidlem44  46472  fourierdlem41  46576  fourierdlem42  46577  fourierdlem51  46585  fourierdlem68  46602  fourierdlem89  46623  fourierdlem91  46625  fourierdlem92  46626  fourierdlem94  46628  etransclem24  46686  etransclem34  46696  qndenserrnbllem  46722  salincl  46752  saldifcl2  46756  subsalsal  46787  sge0pr  46822  sge0pnffigt  46824  sge0reuz  46875  nnfoctbdjlem  46883  nnfoctbdj  46884  meadjiunlem  46893  caratheodorylem2  46955  hoidmv1le  47022  hoidmvlelem3  47025  hspmbllem2  47055  opnvonmbllem2  47061  sssmf  47166  smfaddlem1  47191  sigaraf  47281  sigarmf  47282  nltle2tri  47761  subsubelfzo0  47775  nnmul2  47778  submodaddmod  47795  zplusmodne  47797  addmodne  47798  minusmod5ne  47803  submodneaddmod  47805  modmkpkne  47815  modmknepk  47816  iccpartiltu  47882  icceuelpart  47896  poprelb  47984  reuopreuprim  47986  nprmmul2  47988  proththd  48077  mogoldbblem  48196  fppr2odd  48207  fpprel2  48217  bgoldbtbndlem2  48282  clnbusgrfi  48319  grimuhgr  48363  uhgrimisgrgric  48407  clnbgrgrim  48410  grtrif1o  48418  grlimgrtri  48479  gpgusgralem  48532  gpgedgvtx0  48537  gpgedg2ov  48542  gpgedg2iv  48543  gpg5nbgrvtx03starlem2  48545  nn0sumltlt  48826  invginvrid  48843  ply1sclrmsm  48860  linccl  48890  lincvalpr  48894  lincresunit3lem1  48955  lincresunit3  48957  fdivmpt  49016  nnolog2flm1  49066  dignnld  49079  digexp  49083  dignn0flhalflem1  49091  itcovalsucov  49144  reorelicc  49186  eenglngeehlnmlem1  49213  line2  49228  line2xlem  49229  itsclc0lem1  49232  itsclc0xyqsolr  49245  i0oii  49395  io1ii  49396  indthinc  49937  indthincALT  49938  setrec2fun  50167  reccot  50233  rectan  50234