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  2662  eqeu  3667  onunel  6469  iotan0  6527  funopg  6571  dff1o2  6827  fvelimad  6949  unima  6957  fnimapr  6965  fvmptt  7011  fnreseql  7044  xpprsng  7139  xpsnprg  7140  f1elima  7264  f1ounsn  7277  f13dfv  7279  f1ocnvfvb  7284  f1cdmsn  7287  f1ofvswap  7311  oprssov  7587  resf1extb  7935  resf1ext2b  7936  funelss  8048  poxp  8130  poxp2  8145  poxp3  8152  smoiso  8355  oaord  8538  oaword  8540  omcan  8560  omwordri  8563  odi  8570  omeulem1  8573  oeord  8580  oecan  8581  oewordri  8584  oeordsuc  8586  nnaord  8611  nnaordr  8612  nndi  8615  nnaword  8619  nnmwordri  8628  naddel2  8681  naddss1  8682  naddss2  8683  erov  8818  ecopovtrn  8824  curfv  8875  mapsnd  8897  f1dom3g  8977  xpdom3  9077  mapxpen  9145  dif1en  9160  findcard  9162  f1domfi2  9180  entrfir  9189  domtrfil  9190  domtrfir  9192  sbthfilem  9196  sdomdomtrfi  9199  php3  9207  findcard3  9257  indexfi  9331  suppr  9446  infpr  9479  r111  9761  tcrank  9870  acndom  10058  infdif2  10215  infxpdom  10216  cfeq0  10262  cfsuc  10263  cfflb  10265  cflim2  10269  cfsmolem  10276  axcc3  10444  domtriomlem  10448  axdc3lem2  10457  axdc3lem4  10459  axdc4lem  10461  axcclem  10463  pwcfsdom  10596  tsktrss  10774  tsksuc  10775  tskuni  10796  adderpqlem  10967  mulerpqlem  10968  mulcanenq  10973  distrnq  10974  ltsonq  10982  ltanq  10984  ltmnq  10985  distrlem1pr  11038  distrlem5pr  11040  ltsopr  11045  ltsosr  11107  ltasr  11113  adddir  11225  axlttrn  11310  letr  11332  nnncan1  11522  npncan3  11524  pnpcan2  11526  subdi  11675  subdir  11676  mulcan1g  11895  mulcan2g  11896  divmul  11903  div23  11919  div13  11921  muldivdir  11935  divsubdir  11936  subdivcomb1  11938  divcan7  11952  ltmul2  12094  lemul1  12095  lemul2  12096  lemul2a  12098  lediv1  12108  ltmuldiv2  12117  lemuldiv  12123  lemuldiv2  12124  ltdiv2  12129  lediv2  12133  infrelb  12228  nndivtr  12311  bndndx  12531  nn0n0n1ge2  12600  fnn0ind  12724  addlelt  13162  xrletr  13213  qsqueeze  13257  xleadd2a  13310  xleadd1  13311  xltadd2  13313  xltmul2  13349  supxrbnd  13384  iooneg  13528  iccneg  13529  icoshft  13530  icoshftf1o  13531  zltaddlt1le  13562  fzen  13599  uzsubsubfz  13605  ssfzunsnext  13628  fzrevral2  13672  fzshftral  13674  fz0fzdiffz0  13696  elfzmlbp  13698  elfzo  13720  nelfzo  13724  fzoaddel2  13780  fzosubel2  13785  ssfzo12bi  13821  fzonfzoufzol  13831  subfzo0  13853  flltdivnn0lt  13898  modmulnn  13954  modcyc  13971  modaddabs  13976  modaddmod  13977  modmuladd  13981  modadd2mod  13989  modsubmod  13997  modsubmodmod  13998  modaddmodup  14002  modmulmod  14004  modsubdir  14008  modfzo0difsn  14011  modsumfzodifsn  14012  uzindi  14050  axdc4uzlem  14051  expneg2  14138  expdiv  14181  expubnd  14246  mulbinom2  14291  bernneq2  14298  expnngt1  14309  hashinfxadd  14453  hashunsngx  14461  hashunsnggt  14462  hashfundm  14511  hashf1dmcdm  14513  hashdifsnp1  14575  ccatval3  14648  ccatfv0  14653  ccatval1lsw  14654  ccats1val2  14699  ccatw2s1p1  14708  swrdnd  14728  pfxsuffeqwrdeq  14771  pfxsuff1eqwrdeq  14772  swrdswrd  14778  pfxpfx  14781  wrd2ind  14796  swrdccatin1  14798  pfxccatin12lem1  14801  swrdccatin2  14802  pfxccatin12lem3  14805  swrdccat  14808  pfxccatpfx1  14809  pfxccatpfx2  14810  swrdccat3blem  14812  swrdrevpfx  14842  repswswrd  14859  repswpfx  14860  repswccat  14861  cshwidxmod  14878  2cshw  14888  3cshw  14893  scshwfzeqfzo  14901  cshwcsh2id  14903  cshimadifsn  14904  cshimadifsn0  14905  ccatco  14910  cshco  14911  swrdco  14912  pfxco  14913  lswco  14914  swrds2  15015  2swrd2eqwrdeq  15030  shftuz  15146  sgn3da  15178  abs3dif  15423  fsumdifsnconst  15882  modfsummods  15884  sin02gt0  16286  dvdsval2  16351  dvdscmul  16378  dvdsmulc  16379  dvdscmulr  16380  dvdsmulcr  16381  divalglem8  16496  ndvdssub  16505  dvdsexpim  16651  rpmulgcd  16653  expgcd  16659  zexpgcd  16661  coprmprod  16757  cncongr1  16763  cncongr2  16764  isprm3  16779  modprm0  16903  coprimeprodsq  16906  pythagtriplem12  16924  pythagtriplem14  16926  pcprendvds  16938  pcmul  16949  pcdiv  16950  pcqcl  16954  pcqdiv  16955  pcdvdsb  16967  vdwnnlem1  17093  hashbcss  17102  cshwshashlem1  17193  fvsetsid  17266  setsstruct2  17272  setsstruct  17274  mrcss  17710  mrcsscl  17714  mrcun  17716  cofulid  17985  catcisolem  18205  funcsetcestrclem9  18257  latleeqj1  18545  lubun  18609  clatleglb  18612  pslem  18666  dirtr  18696  mgmb1mgm1  18753  pwspjmhm  18945  grpinvid1  19121  grpinvid2  19122  grpasscan1  19131  grpasscan2  19132  grpinvadd  19147  grpsubf  19148  grpsubrcan  19150  grpinvsub  19151  grpsubeq0  19155  grpsubadd0sub  19156  grppncan  19160  grpnpcan  19161  mulgnn0p1  19214  mulgaddcomlem  19226  mulginvcom  19228  mulginvinv  19229  subgsubcl  19267  subgsub  19268  eqglact  19310  qussub  19325  ghmsub  19357  psgnunilem4  19630  oddvds2  19699  odsubdvds  19704  gexnnod  19721  slwn0  19748  dvrcl  20551  unitdvcl  20552  dvrcan1  20556  dvrcan3  20557  dvreq1  20558  rngisom1  20613  rngisomring  20614  subrgdv  20757  isdrng3lem2  20921  abvsubtri  20999  idsrngd  21028  lmodvsubval2  21107  lsmcl  21273  lsmsp2  21277  lspsntrim  21288  rngqiprngimfolem  21499  lidldvgen  21571  cncrng  21612  chrcong  21746  dvdschrmulg  21747  zndvds  21768  zntoslem  21775  ocvsscon  21894  obselocv  21947  frlmphl  22000  ascldimul  22109  mpfsubrg  22333  ply1tmcl  22504  eqcoe1ply1eq  22530  gsummoncoe1  22539  lply1binomsc  22542  mamudm  22623  mamufacex  22624  scmatf1  22759  scmatf1o  22760  scmatrngiso  22764  submabas  22806  mdetdiaglem  22826  mdetralt2  22837  mdetero  22838  mdetunilem2  22841  mdetunilem6  22845  m2detleiblem7  22855  maducoeval2  22868  gsummatr01lem3  22885  gsummatr01  22887  smadiadetglem2  22900  matunitlindflem1  22907  cramerlem1  22918  mply1topmatcl  23036  mp2pm2mplem4  23040  ntrin  23292  elnei  23342  neindisj2  23354  ordtopn3  23427  leordtval2  23443  lecldbas  23450  cnrest2  23517  cmpsublem  23630  ptrescn  23871  xkococn  23892  kqfeq  23956  snfbas  24098  neifil  24112  fclsrest  24256  utopsnnei  24481  neipcfilu  24527  psmetsym  24542  psmetge0  24544  xmetge0  24576  xmetsym  24579  metustto  24785  metustbl  24798  restmetu  24802  nm2dif  24857  nmtri  24858  cnmet  25003  cnmpopc  25162  iihalf1  25165  iihalf2  25167  iocopnst  25174  clmnegsubdi2  25339  clmsub4  25340  clmvsubval2  25344  ncvspi  25390  cphsqrtcl3  25421  cph2ass  25447  cphipval2  25475  cphipval  25477  caublcls  25543  bcthlem3  25560  bcthlem4  25561  srabn  25594  cssbn  25609  cmslsschl  25611  rrxmet  25642  rrxdsfi  25645  iblconst  26052  dvdsq1p  26395  coeid3  26473  aannenlem2  26572  pserdvlem2  26671  tanord1  26782  cxpef  26910  recxpcl  26920  logbchbase  27016  relogbcl  27018  relogbzcl  27019  logbleb  27028  logblt  27029  relogbcxpb  27032  lawcos  27061  pythag  27062  isosctrlem1  27063  isosctrlem2  27064  lgsmodeq  27586  lgsmulsqcoprm  27587  gausslemma2dlem1a  27609  2lgsoddprmlem2  27653  ltsres  27906  lestr  28006  cofcutr  28197  lrrecpo  28214  ltadds2im  28259  leadds2im  28261  leadds1  28262  leadds2  28263  ltadds1  28265  addscan2  28266  addscan1  28267  ltsubs1  28349  divmulsw  28466  oldfib  28650  zsoring  28682  bdayfinbndlem1  28740  ax5seglem1  29393  axcontlem2  29430  axcontlem8  29436  upgrpredgv  29604  numedglnl  29609  issubgr2  29740  uhgrissubgr  29743  egrsubgr  29745  nbusgrfi  29842  nb3grprlem2  29849  cplgr3v  29903  cusgrsizeindslem  29919  finsumvtxdg2size  30018  rusgrpropadjvtx  30053  upgrwlkvtxedg  30112  swrdwlk  30155  usgr2trlncl  30233  uspgrn2crct  30284  crctcshwlkn0lem4  30289  crctcshwlkn0lem5  30290  wwlksnextproplem3  30387  umgr2adedgwlklem  30420  rusgr0edg  30452  clwwlk1loop  30466  clwwlkccatlem  30467  clwlkclwwlklem2a4  30475  clwlkclwwlklem2a  30476  clwwisshclwwslemlem  30491  erclwwlktr  30500  clwwlkel  30524  erclwwlkntr  30549  clwwlknonex2lem2  30586  uhgr3cyclex  30670  umgr3cyclex  30671  eucrctshift  30731  frgr3v  30763  3cyclfrgrrn  30774  frgrwopreglem5a  30799  frgr2wsp1  30818  extwwlkfab  30840  clwwlknonclwlknonf1o  30850  numclwwlk3lem1  30870  numclwwlk5  30876  numclwwlk6  30878  isgrpo  30986  grpoinvid1  31017  grpoinvid2  31018  grpoinvop  31022  grpodivinv  31025  grpoinvdiv  31026  grpodivf  31027  grponpcan  31032  ablonncan  31045  nvmval  31131  nvmval2  31132  nvmfval  31133  nvmul0or  31139  nvpncan2  31142  nvaddsub4  31146  nvmeq0  31147  nvdif  31155  nvpi  31156  nvmtri  31160  nvabs  31161  imsmetlem  31179  ipval2lem3  31194  ipval2  31196  4ipval2  31197  ipval3  31198  nmooge0  31256  blometi  31292  hvaddsub12  31527  hvsubdistr1  31538  hvsubdistr2  31539  hvaddcan2  31560  hvmulcan  31561  hvmulcan2  31562  hvsubcan  31563  hvsubcan2  31564  his7  31579  his2sub  31581  his2sub2  31582  norm3dif2  31640  shsubcl  31709  hhssnv  31753  shlej2  31850  fh2  32108  cm2j  32109  pjoi0  32206  hodcl  32236  hosubdi  32297  unopf1o  32405  unopadj  32408  adj2  32423  braadd  32434  bramul  32435  lnopaddmuli  32462  lnopsubmuli  32464  homco2  32466  lnfnaddmuli  32534  adjlnop  32575  leopmul  32623  leoptr  32626  pjimai  32665  atcv1  32869  atexch  32870  atcvatlem  32874  fcoinvbr  33086  preiman0  33190  divnumden2  33294  xdivmul  33378  cshf1o  33410  resvsca  33780  idlsrgcmnd  33933  hasheuni  34603  cndprobin  34953  bayesth  34958  signstfvp  35087  breprexplemc  35148  trssfir1om  35629  fineqvac  35650  fineqvnttrclselem1  35655  fineqvnttrclselem3  35657  trssfir1omregs  35670  lediv2aALT  36264  fununiq  36356  dfrdg2  36380  clsun  36955  neiin  36959  rdgeqoa  38132  poimirlem32  38409  ftc1anclem4  38453  areacirc  38470  filbcmb  38498  ismtybnd  38565  grpoeqdivid  38639  ghomco  38649  rngonegrmul  38702  zerdivemp1x  38705  rngohomco  38732  rngoisoco  38740  riscer  38746  intidl  38787  isfldidl  38826  eceldmqsxrncnvepres  39192  eceldmqsxrncnvepres2  39193  brredunds  39466  lshpnelb  39865  opnlen0  40069  opcon3b  40077  opcon2b  40078  oplecon3b  40081  opltcon3b  40085  opltcon2b  40087  oldmm1  40098  oldmm4  40101  oldmj1  40102  oldmj4  40105  cvrval2  40155  cvrcon3b  40158  leatb  40173  atcmp  40192  atcvreq0  40195  atlatle  40201  athgt  40337  3dim2  40349  islln2a  40398  lplnnleat  40423  lvolnleat  40464  4atlem10  40487  4atlem11  40490  4atlem12  40493  dalem21  40575  dalem22  40576  dalem23  40577  dalem29  40582  dalem30  40583  dalem31N  40584  dalem32  40585  dalem33  40586  dalem34  40587  dalem35  40588  dalem36  40589  dalem37  40590  dalem40  40593  dalem46  40599  dalem47  40600  dalem51  40604  dalem52  40605  dalem58  40611  dalem59  40612  pmaple  40642  paddclN  40723  pmapjoin  40733  pmapjat1  40734  elpcliN  40774  pclssN  40775  pclun2N  40780  2polcon4bN  40799  paddunN  40808  poldmj1N  40809  pmapj2N  40810  pmapocjN  40811  psubclinN  40829  paddatclN  40830  poml4N  40834  lautco  40978  ldilco  40997  ltrneq2  41029  trljat1  41047  cdlemc1  41072  cdleme10  41135  ltrnco  41600  trlcocnv  41601  trljco  41621  trljco2  41622  cdlemi1  41699  tendocnv  41902  diaord  41928  dibord  42040  dihord3  42138  dihord4  42139  dihmeetlem2N  42180  dihmeetlem4preN  42187  dochdmj1  42271  hdmap10lem  42720  lcmineqlem1  42903  sticksstones2  43021  readdsub  43267  reltsub1  43269  renpncan3  43274  reppncan  43276  resubdi  43279  readdcan2  43296  mzprename  43602  dvdsrabdioph  43659  pell14qrdivcl  43714  monotoddzz  43792  jm2.19lem2  43839  jm2.19  43842  relexpaddss  44566  k0004lem3  44997  dvconstbi  45166  chordthmALT  45763  isosctrlem1ALT  45764  ssinc  45927  ssdec  45928  wessf1ornlem  46025  disjf1o  46031  ssnnf1octb  46034  projf1o  46036  mapssbi  46051  iunmapsn  46055  upbdrech  46146  iuneqfzuzlem  46172  suplesup  46177  rexabslelem  46254  climxrrelem  46585  limsupresxr  46602  liminfresxr  46603  liminfvalxr  46619  xlimliminflimsup  46698  cncfshift  46710  cncfperiod  46715  cncfuni  46722  icccncfext  46723  dvmptfprodlem  46780  dvnprodlem1  46782  itgspltprt  46815  ismbl3  46822  stoweidlem3  46839  stoweidlem10  46846  stoweidlem19  46855  stoweidlem31  46867  stoweidlem34  46870  stoweidlem44  46880  fourierdlem41  46984  fourierdlem42  46985  fourierdlem51  46993  fourierdlem68  47010  fourierdlem89  47031  fourierdlem91  47033  fourierdlem92  47034  fourierdlem94  47036  etransclem24  47094  etransclem34  47104  qndenserrnbllem  47130  salincl  47160  saldifcl2  47164  subsalsal  47195  sge0pr  47230  sge0pnffigt  47232  sge0reuz  47283  nnfoctbdjlem  47291  nnfoctbdj  47292  meadjiunlem  47301  caratheodorylem2  47363  hoidmv1le  47430  hoidmvlelem3  47433  hspmbllem2  47463  opnvonmbllem2  47469  smfaddlem1  47599  sigaraf  47689  sigarmf  47690  nltle2tri  48209  subsubelfzo0  48223  nnmul2  48226  submodaddmod  48243  zplusmodne  48245  addmodne  48246  minusmod5ne  48251  submodneaddmod  48253  modmkpkne  48263  modmknepk  48264  iccpartiltu  48330  icceuelpart  48344  poprelb  48432  reuopreuprim  48434  nprmmul2  48436  proththd  48525  mogoldbblem  48644  fppr2odd  48655  fpprel2  48665  bgoldbtbndlem2  48730  clnbusgrfi  48767  grimuhgr  48811  uhgrimisgrgric  48855  clnbgrgrim  48858  grtrif1o  48866  grlimgrtri  48927  gpgusgralem  48980  gpgedgvtx0  48985  gpgedg2ov  48990  gpgedg2iv  48991  gpg5nbgrvtx03starlem2  48993  nn0sumltlt  49288  invginvrid  49305  ply1sclrmsm  49322  linccl  49352  lincvalpr  49356  lincresunit3lem1  49417  lincresunit3  49419  fdivmpt  49478  nnolog2flm1  49528  dignnld  49541  digexp  49545  dignn0flhalflem1  49553  itcovalsucov  49606  reorelicc  49648  eenglngeehlnmlem1  49675  line2  49690  line2xlem  49691  itsclc0lem1  49694  itsclc0xyqsolr  49707  i0oii  49854  io1ii  49855  indthinc  50396  indthincALT  50397  setrec2fun  50626  reccot  50692  rectan  50693