Theorem 3adant2 1073

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		3simpb 1052	. 2 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adant.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl 17	1 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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  df-3an 1033

This theorem is referenced by:  3ad2ant1  1075  eupickb  2526  vtoclegft  3253  eqeu  3344  funopg  5836  fnco  5913  dff1o2  6055  fnimapr  6172  fvmptt  6208  fnreseql  6235  f1elima  6421  f13dfv  6430  f1ocnvfvb  6435  oprssov  6701  ordunel  6919  poxp  7176  wfrlem4  7305  smoiso  7346  oaord  7514  oaword  7516  omcan  7536  omwordri  7539  odi  7546  omeulem1  7549  oeord  7555  oecan  7556  oewordri  7559  oeordsuc  7561  nnaord  7586  nnaordr  7587  nndi  7590  nnaword  7594  nnmwordri  7603  erov  7731  ecopovtrn  7737  xpdom3  7943  mapxpen  8011  findcard  8084  indexfi  8157  suppr  8260  infpr  8292  r111  8521  tcrank  8630  acndom  8757  infdif2  8915  infxpdom  8916  cfeq0  8961  cfsuc  8962  cfflb  8964  cflim2  8968  cfsmolem  8975  axcc3  9143  domtriomlem  9147  axdc3lem2  9156  axdc3lem4  9158  axdc4lem  9160  axcclem  9162  pwcfsdom  9284  tsktrss  9462  tsksuc  9463  tskuni  9484  adderpqlem  9655  mulerpqlem  9656  mulcanenq  9661  distrnq  9662  ltsonq  9670  ltanq  9672  ltmnq  9673  distrlem1pr  9726  distrlem5pr  9728  ltsopr  9733  ltsosr  9794  ltasr  9800  adddir  9910  axlttrn  9989  letr  10010  nnncan1  10196  npncan3  10198  pnpcan2  10200  subdi  10342  subdir  10343  mulcan1g  10559  mulcan2g  10560  divmul  10567  div23  10583  div13  10585  muldivdir  10599  divsubdir  10600  divcan7  10613  ltmul2  10753  lemul1  10754  lemul2  10755  lemul2a  10757  lediv1  10767  ltmuldiv2  10776  lemuldiv  10782  lemuldiv2  10783  ltdiv2  10788  lediv2  10792  fiminre  10851  infrelb  10885  nndivtr  10939  bndndx  11168  nn0n0n1ge2  11235  fnn0ind  11352  addlelt  11818  xrletr  11865  qsqueeze  11906  xleadd2a  11956  xleadd1  11957  xltadd2  11959  xltmul2  11995  supxrbnd  12030  iooneg  12163  iccneg  12164  icoshft  12165  icoshftf1o  12166  zltaddlt1le  12195  fzen  12229  uzsubsubfz  12234  fzrevral2  12295  fzshftral  12297  fz0fzdiffz0  12317  elfzmlbp  12319  elfzo  12341  nelfzo  12344  fzoaddel2  12391  fzosubel2  12395  elfzom1p1elfzo  12414  ssfzo12bi  12429  fzonfzoufzol  12437  subfzo0  12452  flltdivnn0lt  12496  modmulnn  12550  modcyc  12567  modaddabs  12570  modaddmod  12571  modmuladd  12574  modadd2mod  12582  modsubmod  12590  modsubmodmod  12591  modaddmodup  12595  modmulmod  12597  moddi  12600  modsubdir  12601  modfzo0difsn  12604  modsumfzodifsn  12605  uzindi  12643  axdc4uzlem  12644  expneg2  12731  expdiv  12773  expubnd  12783  mulbinom2  12846  bernneq2  12853  hashinfxadd  13035  brfi1indlem  13133  ccatval3  13216  ccatsymb  13219  ccatfv0  13220  ccatval1lsw  13221  ccats1val2  13256  swrdnd  13284  2swrd1eqwrdeq  13306  swrdswrd  13312  wrd2ind  13329  swrdccatin1  13334  swrdccatin12lem2b  13337  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12lem3  13341  swrdccat  13344  swrdccat3a  13345  swrdccat3blem  13346  repswswrd  13382  repswccat  13383  cshwidxmod  13400  2cshw  13410  3cshw  13415  scshwfzeqfzo  13423  cshwcsh2id  13425  cshimadifsn  13426  cshimadifsn0  13427  ccatco  13432  cshco  13433  swrdco  13434  lswco  13435  swrds2  13533  2swrd2eqwrdeq  13544  shftuz  13657  shftval2  13663  abs3dif  13919  modfsummods  14366  sin02gt0  14761  dvdsval2  14824  dvdscmul  14846  dvdsmulc  14847  dvdscmulr  14848  dvdsmulcr  14849  mulmoddvds  14889  divalglem8  14961  ndvdssub  14971  rpmulgcd  15113  coprmdvdsOLD  15205  coprmprod  15213  cncongr1  15219  cncongr2  15220  isprm3  15234  modprm0  15348  coprimeprodsq  15351  pythagtriplem12  15369  pythagtriplem14  15371  pcprendvds  15383  pcmul  15394  pcdiv  15395  pcqcl  15399  pcqdiv  15400  pcdvdsb  15411  pcgcd  15420  vdwnnlem1  15537  hashbcss  15546  cshwshashlem1  15640  fvsetsid  15722  mrcss  16099  mrcsscl  16103  mrcun  16105  cofulid  16373  catcisolem  16579  funcsetcestrclem9  16626  latleeqj1  16886  lubun  16946  clatleglb  16949  pslem  17029  dirtr  17059  mgmb1mgm1  17077  pwspjmhm  17191  gsumccat  17201  grpinvid1  17293  grpinvid2  17294  grpasscan1  17301  grpasscan2  17302  grpinvadd  17316  grpsubf  17317  grpsubrcan  17319  grpinvsub  17320  grpsubeq0  17324  grpsubadd0sub  17325  grppncan  17329  grpnpcan  17330  mulgnn0p1  17375  mulgaddcomlem  17386  mulginvcom  17388  mulginvinv  17389  subgsubcl  17428  subgsub  17429  eqglact  17468  qussub  17477  ghmsub  17491  psgnunilem4  17740  oddvds2  17806  odsubdvds  17809  gexnnod  17826  slwn0  17853  gsumdixp  18432  dvrcl  18509  unitdvcl  18510  dvrcan1  18514  dvrcan3  18515  dvreq1  18516  subrgdv  18620  abvsubtri  18658  idsrngd  18685  lmodvsubval2  18741  lsmcl  18904  lsmsp2  18908  lspsntrim  18919  lidldvgen  19076  evlslem4  19329  mpfsubrg  19353  ply1tmcl  19463  eqcoe1ply1eq  19488  gsummoncoe1  19495  lply1binomsc  19498  chrcong  19696  zndvds  19717  zntoslem  19724  ocvsscon  19838  obselocv  19891  frlmphl  19939  mamudm  20013  mamufacex  20014  scmatf1  20156  scmatf1o  20157  scmatrngiso  20161  submabas  20203  mdetdiaglem  20223  mdetralt2  20234  mdetero  20235  mdetunilem2  20238  mdetunilem6  20242  m2detleiblem7  20252  maducoeval2  20265  gsummatr01lem3  20282  gsummatr01  20284  smadiadetglem2  20297  cramerlem1  20312  mply1topmatcl  20429  mp2pm2mplem4  20433  ntrin  20675  elnei  20725  neindisj2  20737  ordtopn3  20810  ordtcld3  20813  leordtval2  20826  lecldbas  20833  cnrest2  20900  cmpsublem  21012  ptrescn  21252  xkococn  21273  kqfeq  21337  snfbas  21480  neifil  21494  fclsrest  21638  utopsnnei  21863  neipcfilu  21910  psmetsym  21925  psmetge0  21927  xmetge0  21959  xmetsym  21962  metustto  22168  metustbl  22181  restmetu  22185  nm2dif  22239  nmtri  22240  cnmet  22385  cnmpt2pc  22535  iihalf1  22538  iihalf2  22540  iocopnst  22547  clmnegsubdi2  22713  clmsub4  22714  clmvsubval2  22718  ncvspi  22764  cphsqrtcl3  22795  cph2ass  22821  cphipval2  22848  cphipval  22850  caublcls  22915  bcthlem3  22931  bcthlem4  22932  srabn  22964  rrxmet  22999  iblconst  23390  tdeglem3  23623  mdegmullem  23642  dvdsq1p  23724  coeid3  23800  aannenlem2  23888  pserdvlem2  23986  tanord1  24087  cxpef  24211  recxpcl  24221  logbchbase  24309  relogbcl  24311  relogbzcl  24312  logbleb  24321  logblt  24322  relogbcxpb  24325  lawcos  24346  pythag  24347  isosctrlem1  24348  isosctrlem2  24349  lgsmodeq  24867  lgsmulsqcoprm  24868  gausslemma2dlem1a  24890  2lgsoddprmlem2  24934  ax5seglem1  25608  axcontlem2  25645  axcontlem8  25651  fiusgraedgfi  25936  nbgraf1olem3  25972  nb3graprlem2  25981  cusgra3v  25993  cusgrasizeindslem2  26003  cusgrasizeinds  26004  iswlkon  26062  istrlon  26071  2trllemE  26083  usgrwlknloop  26093  ispthon  26106  isspthon  26113  usgra2adedgwlkonALT  26144  usgrcyclnl2  26169  3v3e3cycl1  26172  constr3lem4  26175  constr3lem5  26176  constr3lem6  26177  constr3trllem2  26179  constr3trllem3  26180  4cycl4dv  26195  wwlkextproplem3  26271  clwwlkgt0  26299  clwwlknndef  26301  clwwlknfi  26306  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwwlkel  26321  clwwlkext2edg  26330  clwwisshclwwlem1  26333  clwwnisshclwwn  26337  erclwwlktr  26343  erclwwlkntr  26355  clwlkfclwwlk  26371  clwlkfoclwwlk  26372  usg2wotspth  26411  2spontn0vne  26414  nbhashnn0  26441  nbhashuvtx  26443  usgrauvtxvdbi  26447  rusgra0edg  26482  frgra3v  26529  usg2spot2nb  26592  numclwlk3lem3  26600  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwwlkovgelim  26616  numclwwlk4  26637  numclwwlk5lem  26638  numclwwlk5  26639  numclwwlk6  26640  numclwwlk7  26641  isgrpo  26735  grpoinvid1  26766  grpoinvid2  26767  grpoinvop  26771  grpodivinv  26774  grpoinvdiv  26775  grpodivf  26776  grponpcan  26781  ablonncan  26795  nvmval  26881  nvmval2  26882  nvmfval  26883  nvmul0or  26889  nvpncan2  26892  nvaddsub4  26896  nvmeq0  26897  nvdif  26905  nvpi  26906  nvmtri  26910  nvabs  26911  imsmetlem  26929  ipval2lem3  26944  ipval2  26946  4ipval2  26947  ipval3  26948  nmooge0  27006  blometi  27042  hvaddsub12  27279  hvsubdistr1  27290  hvsubdistr2  27291  hvaddcan2  27312  hvmulcan  27313  hvmulcan2  27314  hvsubcan  27315  hvsubcan2  27316  his7  27331  his2sub  27333  his2sub2  27334  norm3dif2  27392  shsubcl  27461  hhssnv  27505  shlej2  27604  fh2  27862  cm2j  27863  pjoi0  27960  hodcl  27990  hosubdi  28051  unopf1o  28159  unopadj  28162  adj2  28177  braadd  28188  bramul  28189  lnopaddmuli  28216  lnopsubmuli  28218  homco2  28220  lnfnaddmuli  28288  adjlnop  28329  leopmul  28377  leoptr  28380  pjimai  28419  atcv1  28623  atexch  28624  atcvatlem  28628  fcoinvbr  28799  divnumden2  28951  xdivmul  28964  resvsca  29161  hasheuni  29474  difelsiga  29523  cndprobin  29823  bayesth  29828  sgn3da  29930  lediv2aALT  30825  subdivcomb1  30864  fununiq  30913  dfrdg2  30945  sltres  31061  nobndlem8  31098  clsun  31493  neiin  31497  rdgeqoa  32394  curfv  32559  matunitlindflem1  32575  poimirlem32  32611  ftc1anclem4  32658  areacirc  32675  filbcmb  32705  ismtybnd  32776  grpoeqdivid  32850  ghomco  32860  rngonegrmul  32913  zerdivemp1x  32916  rngohomco  32943  rngoisoco  32951  riscer  32957  intidl  32998  isfldidl  33037  lshpnelb  33289  opnlen0  33493  opcon3b  33501  opcon2b  33502  oplecon3b  33505  opltcon3b  33509  opltcon2b  33511  oldmm1  33522  oldmm4  33525  oldmj1  33526  oldmj4  33529  cvrval2  33579  cvrcon3b  33582  leatb  33597  atcmp  33616  atcvreq0  33619  atlatle  33625  athgt  33760  3dim2  33772  islln2a  33821  lplnnleat  33846  lvolnleat  33887  4atlem10  33910  4atlem11  33913  4atlem12  33916  dalem21  33998  dalem22  33999  dalem23  34000  dalem29  34005  dalem30  34006  dalem31N  34007  dalem32  34008  dalem33  34009  dalem34  34010  dalem35  34011  dalem36  34012  dalem37  34013  dalem40  34016  dalem46  34022  dalem47  34023  dalem51  34027  dalem52  34028  dalem58  34034  dalem59  34035  pmaple  34065  paddclN  34146  pmapjoin  34156  pmapjat1  34157  elpcliN  34197  pclssN  34198  pclun2N  34203  2polcon4bN  34222  paddunN  34231  poldmj1N  34232  pmapj2N  34233  pmapocjN  34234  psubclinN  34252  paddatclN  34253  poml4N  34257  lautco  34401  ldilco  34420  ltrneq2  34452  trljat1  34471  cdlemc1  34496  cdleme10  34559  ltrnco  35025  trlcocnv  35026  trljco  35046  trljco2  35047  cdlemi1  35124  tendocnv  35328  diaord  35354  dibord  35466  dihord3  35564  dihord4  35565  dihmeetlem2N  35606  dihmeetlem4preN  35613  dochdmj1  35697  hdmap10lem  36149  mzprename  36330  dvdsrabdioph  36392  pell14qrdivcl  36447  monotoddzz  36526  jm2.19lem2  36575  jm2.19  36578  relexpaddss  37029  k0004lem3  37467  dvconstbi  37555  chordthmALT  38191  isosctrlem1ALT  38192  ssinc  38292  ssdec  38293  eliuniin  38307  eliuniin2  38335  unima  38340  wessf1ornlem  38366  disjf1o  38373  disjinfi  38375  ssnnf1octb  38377  projf1o  38381  mapsnd  38383  mapssbi  38400  iunmapsn  38404  upbdrech  38460  iuneqfzuzlem  38491  suplesup  38496  cncfshift  38759  cncfperiod  38764  cncfuni  38772  icccncfext  38773  dvmptfprodlem  38834  dvnprodlem1  38836  itgspltprt  38871  ismbl3  38879  stoweidlem3  38896  stoweidlem10  38903  stoweidlem19  38912  stoweidlem31  38924  stoweidlem34  38927  stoweidlem44  38937  fourierdlem41  39041  fourierdlem42  39042  fourierdlem51  39050  fourierdlem68  39067  fourierdlem89  39088  fourierdlem91  39090  fourierdlem92  39091  fourierdlem94  39093  etransclem24  39151  etransclem34  39161  rrxdsfi  39181  qndenserrnbllem  39190  salincl  39219  saldifcl2  39222  subsalsal  39253  sge0pr  39287  sge0pnffigt  39289  sge0reuz  39340  nnfoctbdjlem  39348  nnfoctbdj  39349  meadjiunlem  39358  caratheodorylem2  39417  hoidmv1le  39484  hoidmvlelem3  39487  hspmbllem2  39517  opnvonmbllem2  39523  sssmf  39625  smfaddlem1  39649  sigaraf  39691  sigarmf  39692  nltle2tri  39942  iccpartiltu  39960  icceuelpart  39974  proththd  40069  bgoldbtbndlem2  40222  pfxsuffeqwrdeq  40269  pfxsuff1eqwrdeq  40270  ccatpfx  40272  pfxpfx  40278  pfxccatin12lem1  40286  pfxccatpfx1  40290  pfxccatpfx2  40291  repswpfx  40299  pfxco  40301  subsubelfzo0  40359  issubgr2  40496  uhgrissubgr  40499  egrsubgr  40501  fusgrfisstep  40548  nbusgrfi  40602  nb3grprlem2  40609  cplgr3v  40657  cusgrsizeindslem  40667  rusgrpropadjvtx  40785  upgr1wlkvtxedg  40853  usgr2trlncl  40966  uspgrn2crct  41011  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  wwlksnextproplem3  41117  umgr2adedgwlklem  41151  rusgr0edg  41176  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwwlks1loop  41215  clwwlksn1loop  41216  clwwlksel  41221  clwwisshclwwslemlem  41233  erclwwlkstr  41243  erclwwlksntr  41255  clwlksfclwwlk  41269  uhgr3cyclex  41349  umgr3cyclex  41350  eucrctshift  41411  frgr3v  41445  3cyclfrgrrn  41456  fusgr2wsp2nb  41498  av-numclwlk3lem3  41506  av-numclwwlkovf2ex  41517  av-extwwlkfab  41520  av-numclwwlk5  41542  av-numclwwlk6  41544  xpprsng  41903  nn0sumltlt  41921  invginvrid  41942  ply1sclrmsm  41965  linccl  41997  lincvalpr  42001  lincresunit3lem1  42062  lincresunit3  42064  fdivmpt  42132  nnolog2flm1  42182  dignnld  42195  digexp  42199  dignn0flhalflem1  42207  setrec2fun  42238  reccot  42298  rectan  42299