Theorem 3adant2 1149

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 728	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	3impa 1127	1 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3ad2ant1  1151  3simpb  1167  3imp3i2an  1364  eupickb  2666  eqeu  3672  onunel  6475  iotan0  6533  funopg  6577  dff1o2  6833  fvelimad  6955  unima  6963  fnimapr  6971  fvmptt  7017  fnreseql  7050  xpprsng  7143  f1elima  7268  f1ounsn  7281  f13dfv  7283  f1ocnvfvb  7288  f1cdmsn  7291  f1ofvswap  7315  oprssov  7592  resf1extb  7940  resf1ext2b  7941  funelss  8053  poxp  8133  poxp2  8148  poxp3  8155  smoiso  8358  oaord  8541  oaword  8543  omcan  8563  omwordri  8566  odi  8573  omeulem1  8576  oeord  8583  oecan  8584  oewordri  8587  oeordsuc  8589  nnaord  8614  nnaordr  8615  nndi  8618  nnaword  8622  nnmwordri  8631  naddel2  8684  naddss1  8685  naddss2  8686  erov  8821  ecopovtrn  8827  mapsnd  8893  f1dom3g  8973  xpdom3  9073  mapxpen  9141  dif1en  9156  findcard  9158  f1domfi2  9176  entrfir  9185  domtrfil  9186  domtrfir  9188  sbthfilem  9192  sdomdomtrfi  9195  php3  9203  findcard3  9253  indexfi  9327  suppr  9442  infpr  9475  r111  9757  tcrank  9866  acndom  10054  infdif2  10211  infxpdom  10212  cfeq0  10258  cfsuc  10259  cfflb  10261  cflim2  10265  cfsmolem  10272  axcc3  10440  domtriomlem  10444  axdc3lem2  10453  axdc3lem4  10455  axdc4lem  10457  axcclem  10459  pwcfsdom  10586  tsktrss  10764  tsksuc  10765  tskuni  10786  adderpqlem  10957  mulerpqlem  10958  mulcanenq  10963  distrnq  10964  ltsonq  10972  ltanq  10974  ltmnq  10975  distrlem1pr  11028  distrlem5pr  11030  ltsopr  11035  ltsosr  11097  ltasr  11103  adddir  11215  axlttrn  11300  letr  11322  nnncan1  11512  npncan3  11514  pnpcan2  11516  subdi  11665  subdir  11666  mulcan1g  11885  mulcan2g  11886  divmul  11893  div23  11909  div13  11911  muldivdir  11925  divsubdir  11926  subdivcomb1  11928  divcan7  11942  ltmul2  12084  lemul1  12085  lemul2  12086  lemul2a  12088  lediv1  12098  ltmuldiv2  12107  lemuldiv  12113  lemuldiv2  12114  ltdiv2  12119  lediv2  12123  infrelb  12218  nndivtr  12301  bndndx  12521  nn0n0n1ge2  12590  fnn0ind  12713  addlelt  13150  xrletr  13201  qsqueeze  13245  xleadd2a  13298  xleadd1  13299  xltadd2  13301  xltmul2  13337  supxrbnd  13372  iooneg  13516  iccneg  13517  icoshft  13518  icoshftf1o  13519  zltaddlt1le  13550  fzen  13587  uzsubsubfz  13593  ssfzunsnext  13616  fzrevral2  13660  fzshftral  13662  fz0fzdiffz0  13684  elfzmlbp  13686  elfzo  13708  nelfzo  13712  fzoaddel2  13768  fzosubel2  13773  ssfzo12bi  13809  fzonfzoufzol  13819  subfzo0  13841  flltdivnn0lt  13886  modmulnn  13942  modcyc  13959  modaddabs  13964  modaddmod  13965  modmuladd  13969  modadd2mod  13977  modsubmod  13985  modsubmodmod  13986  modaddmodup  13990  modmulmod  13992  modsubdir  13996  modfzo0difsn  13999  modsumfzodifsn  14000  uzindi  14038  axdc4uzlem  14039  expneg2  14126  expdiv  14169  expubnd  14234  mulbinom2  14279  bernneq2  14286  expnngt1  14297  hashinfxadd  14441  hashunsngx  14449  hashunsnggt  14450  hashfundm  14499  hashf1dmcdm  14501  hashdifsnp1  14563  ccatval3  14636  ccatfv0  14641  ccatval1lsw  14642  ccats1val2  14687  ccatw2s1p1  14696  swrdnd  14716  pfxsuffeqwrdeq  14759  pfxsuff1eqwrdeq  14760  swrdswrd  14766  pfxpfx  14769  wrd2ind  14784  swrdccatin1  14786  pfxccatin12lem1  14789  swrdccatin2  14790  pfxccatin12lem3  14793  swrdccat  14796  pfxccatpfx1  14797  pfxccatpfx2  14798  swrdccat3blem  14800  swrdrevpfx  14830  repswswrd  14847  repswpfx  14848  repswccat  14849  cshwidxmod  14866  2cshw  14876  3cshw  14881  scshwfzeqfzo  14889  cshwcsh2id  14891  cshimadifsn  14892  cshimadifsn0  14893  ccatco  14898  cshco  14899  swrdco  14900  pfxco  14901  lswco  14902  swrds2  15003  2swrd2eqwrdeq  15016  shftuz  15132  sgn3da  15164  abs3dif  15409  fsumdifsnconst  15869  modfsummods  15871  sin02gt0  16273  dvdsval2  16338  dvdscmul  16365  dvdsmulc  16366  dvdscmulr  16367  dvdsmulcr  16368  divalglem8  16483  ndvdssub  16492  dvdsexpim  16638  rpmulgcd  16640  expgcd  16646  zexpgcd  16648  coprmprod  16744  cncongr1  16750  cncongr2  16751  isprm3  16766  modprm0  16890  coprimeprodsq  16893  pythagtriplem12  16911  pythagtriplem14  16913  pcprendvds  16925  pcmul  16936  pcdiv  16937  pcqcl  16941  pcqdiv  16942  pcdvdsb  16954  vdwnnlem1  17080  hashbcss  17089  cshwshashlem1  17180  fvsetsid  17253  setsstruct2  17259  setsstruct  17261  mrcss  17697  mrcsscl  17701  mrcun  17703  cofulid  17972  catcisolem  18192  funcsetcestrclem9  18244  latleeqj1  18532  lubun  18596  clatleglb  18599  pslem  18653  dirtr  18683  mgmb1mgm1  18738  pwspjmhm  18920  grpinvid1  19089  grpinvid2  19090  grpasscan1  19099  grpasscan2  19100  grpinvadd  19115  grpsubf  19116  grpsubrcan  19118  grpinvsub  19119  grpsubeq0  19123  grpsubadd0sub  19124  grppncan  19128  grpnpcan  19129  mulgnn0p1  19182  mulgaddcomlem  19194  mulginvcom  19196  mulginvinv  19197  subgsubcl  19235  subgsub  19236  eqglact  19278  qussub  19293  ghmsub  19325  psgnunilem4  19598  oddvds2  19667  odsubdvds  19672  gexnnod  19689  slwn0  19716  dvrcl  20519  unitdvcl  20520  dvrcan1  20524  dvrcan3  20525  dvreq1  20526  rngisom1  20581  rngisomring  20582  subrgdv  20725  isdrng3lem2  20889  abvsubtri  20967  idsrngd  20996  lmodvsubval2  21075  lsmcl  21241  lsmsp2  21245  lspsntrim  21256  rngqiprngimfolem  21467  lidldvgen  21539  cncrng  21580  chrcong  21714  dvdschrmulg  21715  zndvds  21736  zntoslem  21743  ocvsscon  21862  obselocv  21915  frlmphl  21968  ascldimul  22075  mpfsubrg  22299  ply1tmcl  22470  eqcoe1ply1eq  22496  gsummoncoe1  22505  lply1binomsc  22508  mamudm  22589  mamufacex  22590  scmatf1  22725  scmatf1o  22726  scmatrngiso  22730  submabas  22772  mdetdiaglem  22792  mdetralt2  22803  mdetero  22804  mdetunilem2  22807  mdetunilem6  22811  m2detleiblem7  22821  maducoeval2  22834  gsummatr01lem3  22851  gsummatr01  22853  smadiadetglem2  22866  cramerlem1  22881  mply1topmatcl  22999  mp2pm2mplem4  23003  ntrin  23255  elnei  23305  neindisj2  23317  ordtopn3  23390  leordtval2  23406  lecldbas  23413  cnrest2  23480  cmpsublem  23593  ptrescn  23833  xkococn  23854  kqfeq  23918  snfbas  24060  neifil  24074  fclsrest  24218  utopsnnei  24443  neipcfilu  24489  psmetsym  24504  psmetge0  24506  xmetge0  24538  xmetsym  24541  metustto  24747  metustbl  24760  restmetu  24764  nm2dif  24819  nmtri  24820  cnmet  24965  cnmpopc  25124  iihalf1  25127  iihalf2  25129  iocopnst  25136  clmnegsubdi2  25301  clmsub4  25302  clmvsubval2  25306  ncvspi  25352  cphsqrtcl3  25383  cph2ass  25409  cphipval2  25437  cphipval  25439  caublcls  25505  bcthlem3  25522  bcthlem4  25523  srabn  25556  cssbn  25571  cmslsschl  25573  rrxmet  25604  rrxdsfi  25607  iblconst  26014  dvdsq1p  26357  coeid3  26434  aannenlem2  26529  pserdvlem2  26628  tanord1  26739  cxpef  26867  recxpcl  26877  logbchbase  26973  relogbcl  26975  relogbzcl  26976  logbleb  26985  logblt  26986  relogbcxpb  26989  lawcos  27018  pythag  27019  isosctrlem1  27020  isosctrlem2  27021  lgsmodeq  27543  lgsmulsqcoprm  27544  gausslemma2dlem1a  27566  2lgsoddprmlem2  27610  ltsres  27863  lestr  27963  cofcutr  28154  lrrecpo  28171  ltadds2im  28216  leadds2im  28218  leadds1  28219  leadds2  28220  ltadds1  28222  addscan2  28223  addscan1  28224  ltsubs1  28306  divmulsw  28423  oldfib  28607  zsoring  28639  bdayfinbndlem1  28697  ax5seglem1  29315  axcontlem2  29352  axcontlem8  29358  upgrpredgv  29526  numedglnl  29531  issubgr2  29659  uhgrissubgr  29662  egrsubgr  29664  nbusgrfi  29761  nb3grprlem2  29768  cplgr3v  29822  cusgrsizeindslem  29838  finsumvtxdg2size  29937  rusgrpropadjvtx  29972  upgrwlkvtxedg  30031  usgr2trlncl  30146  uspgrn2crct  30194  crctcshwlkn0lem4  30199  crctcshwlkn0lem5  30200  wwlksnextproplem3  30297  umgr2adedgwlklem  30330  rusgr0edg  30362  clwwlk1loop  30376  clwwlkccatlem  30377  clwlkclwwlklem2a4  30385  clwlkclwwlklem2a  30386  clwwisshclwwslemlem  30401  erclwwlktr  30410  clwwlkel  30434  erclwwlkntr  30459  clwwlknonex2lem2  30496  uhgr3cyclex  30570  umgr3cyclex  30571  eucrctshift  30631  frgr3v  30663  3cyclfrgrrn  30674  frgrwopreglem5a  30699  frgr2wsp1  30718  extwwlkfab  30740  clwwlknonclwlknonf1o  30750  numclwwlk3lem1  30770  numclwwlk5  30776  numclwwlk6  30778  isgrpo  30886  grpoinvid1  30917  grpoinvid2  30918  grpoinvop  30922  grpodivinv  30925  grpoinvdiv  30926  grpodivf  30927  grponpcan  30932  ablonncan  30945  nvmval  31031  nvmval2  31032  nvmfval  31033  nvmul0or  31039  nvpncan2  31042  nvaddsub4  31046  nvmeq0  31047  nvdif  31055  nvpi  31056  nvmtri  31060  nvabs  31061  imsmetlem  31079  ipval2lem3  31094  ipval2  31096  4ipval2  31097  ipval3  31098  nmooge0  31156  blometi  31192  hvaddsub12  31427  hvsubdistr1  31438  hvsubdistr2  31439  hvaddcan2  31460  hvmulcan  31461  hvmulcan2  31462  hvsubcan  31463  hvsubcan2  31464  his7  31479  his2sub  31481  his2sub2  31482  norm3dif2  31540  shsubcl  31609  hhssnv  31653  shlej2  31750  fh2  32008  cm2j  32009  pjoi0  32106  hodcl  32136  hosubdi  32197  unopf1o  32305  unopadj  32308  adj2  32323  braadd  32334  bramul  32335  lnopaddmuli  32362  lnopsubmuli  32364  homco2  32366  lnfnaddmuli  32434  adjlnop  32475  leopmul  32523  leoptr  32526  pjimai  32565  atcv1  32769  atexch  32770  atcvatlem  32774  fcoinvbr  32987  preiman0  33092  divnumden2  33197  xdivmul  33281  cshf1o  33313  resvsca  33683  idlsrgcmnd  33836  hasheuni  34506  cndprobin  34856  bayesth  34861  signstfvp  34990  breprexplemc  35051  trssfir1om  35532  fineqvac  35553  fineqvnttrclselem1  35558  fineqvnttrclselem3  35560  trssfir1omregs  35573  swrdwlk  35640  lediv2aALT  36190  fununiq  36282  dfrdg2  36306  clsun  36880  neiin  36884  rdgeqoa  38057  curfv  38292  matunitlindflem1  38308  poimirlem32  38344  ftc1anclem4  38388  areacirc  38405  filbcmb  38432  ismtybnd  38499  grpoeqdivid  38573  ghomco  38583  rngonegrmul  38636  zerdivemp1x  38639  rngohomco  38666  rngoisoco  38674  riscer  38680  intidl  38721  isfldidl  38760  eceldmqsxrncnvepres  39126  eceldmqsxrncnvepres2  39127  brredunds  39400  lshpnelb  39799  opnlen0  40003  opcon3b  40011  opcon2b  40012  oplecon3b  40015  opltcon3b  40019  opltcon2b  40021  oldmm1  40032  oldmm4  40035  oldmj1  40036  oldmj4  40039  cvrval2  40089  cvrcon3b  40092  leatb  40107  atcmp  40126  atcvreq0  40129  atlatle  40135  athgt  40271  3dim2  40283  islln2a  40332  lplnnleat  40357  lvolnleat  40398  4atlem10  40421  4atlem11  40424  4atlem12  40427  dalem21  40509  dalem22  40510  dalem23  40511  dalem29  40516  dalem30  40517  dalem31N  40518  dalem32  40519  dalem33  40520  dalem34  40521  dalem35  40522  dalem36  40523  dalem37  40524  dalem40  40527  dalem46  40533  dalem47  40534  dalem51  40538  dalem52  40539  dalem58  40545  dalem59  40546  pmaple  40576  paddclN  40657  pmapjoin  40667  pmapjat1  40668  elpcliN  40708  pclssN  40709  pclun2N  40714  2polcon4bN  40733  paddunN  40742  poldmj1N  40743  pmapj2N  40744  pmapocjN  40745  psubclinN  40763  paddatclN  40764  poml4N  40768  lautco  40912  ldilco  40931  ltrneq2  40963  trljat1  40981  cdlemc1  41006  cdleme10  41069  ltrnco  41534  trlcocnv  41535  trljco  41555  trljco2  41556  cdlemi1  41633  tendocnv  41836  diaord  41862  dibord  41974  dihord3  42072  dihord4  42073  dihmeetlem2N  42114  dihmeetlem4preN  42121  dochdmj1  42205  hdmap10lem  42654  lcmineqlem1  42837  sticksstones2  42955  readdsub  43186  reltsub1  43188  renpncan3  43193  reppncan  43195  resubdi  43198  readdcan2  43215  mzprename  43521  dvdsrabdioph  43578  pell14qrdivcl  43633  monotoddzz  43711  jm2.19lem2  43758  jm2.19  43761  relexpaddss  44485  k0004lem3  44916  dvconstbi  45085  chordthmALT  45682  isosctrlem1ALT  45683  ssinc  45846  ssdec  45847  wessf1ornlem  45944  disjf1o  45950  ssnnf1octb  45953  projf1o  45955  mapssbi  45970  iunmapsn  45974  upbdrech  46065  iuneqfzuzlem  46091  suplesup  46096  rexabslelem  46173  climxrrelem  46504  limsupresxr  46521  liminfresxr  46522  liminfvalxr  46538  xlimliminflimsup  46617  cncfshift  46629  cncfperiod  46634  cncfuni  46641  icccncfext  46642  dvmptfprodlem  46699  dvnprodlem1  46701  itgspltprt  46734  ismbl3  46741  stoweidlem3  46758  stoweidlem10  46765  stoweidlem19  46774  stoweidlem31  46786  stoweidlem34  46789  stoweidlem44  46799  fourierdlem41  46903  fourierdlem42  46904  fourierdlem51  46912  fourierdlem68  46929  fourierdlem89  46950  fourierdlem91  46952  fourierdlem92  46953  fourierdlem94  46955  etransclem24  47013  etransclem34  47023  qndenserrnbllem  47049  salincl  47079  saldifcl2  47083  subsalsal  47114  sge0pr  47149  sge0pnffigt  47151  sge0reuz  47202  nnfoctbdjlem  47210  nnfoctbdj  47211  meadjiunlem  47220  caratheodorylem2  47282  hoidmv1le  47349  hoidmvlelem3  47352  hspmbllem2  47382  opnvonmbllem2  47388  smfaddlem1  47518  sigaraf  47608  sigarmf  47609  nltle2tri  48091  subsubelfzo0  48105  nnmul2  48108  submodaddmod  48125  zplusmodne  48127  addmodne  48128  minusmod5ne  48133  submodneaddmod  48135  modmkpkne  48145  modmknepk  48146  iccpartiltu  48212  icceuelpart  48226  poprelb  48314  reuopreuprim  48316  nprmmul2  48318  proththd  48407  mogoldbblem  48526  fppr2odd  48537  fpprel2  48547  bgoldbtbndlem2  48612  clnbusgrfi  48649  grimuhgr  48693  uhgrimisgrgric  48737  clnbgrgrim  48740  grtrif1o  48748  grlimgrtri  48809  gpgusgralem  48862  gpgedgvtx0  48867  gpgedg2ov  48872  gpgedg2iv  48873  gpg5nbgrvtx03starlem2  48875  nn0sumltlt  49171  invginvrid  49188  ply1sclrmsm  49205  linccl  49235  lincvalpr  49239  lincresunit3lem1  49300  lincresunit3  49302  fdivmpt  49361  nnolog2flm1  49411  dignnld  49424  digexp  49428  dignn0flhalflem1  49436  itcovalsucov  49489  reorelicc  49531  eenglngeehlnmlem1  49558  line2  49573  line2xlem  49574  itsclc0lem1  49577  itsclc0xyqsolr  49590  i0oii  49739  io1ii  49740  indthinc  50281  indthincALT  50282  setrec2fun  50511  reccot  50577  rectan  50578