Theorem adantrl 729

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

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

Assertion

Ref	Expression
adantrl	⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		simpr 490	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 605	1 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

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

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

This theorem is used by:  ad2ant2l  759  ad2ant2rl  762  cases2ALT  1064  consensus  1068  3ad2antr2  1208  3ad2antr3  1209  po2ne  5582  opabssxpd  5705  frpoind  6371  ordelord  6410  f1un  6875  fvelima2  6968  f1cofveqaeqALT  7293  isocnv  7369  isores2  7372  f1oiso2  7391  offval  7734  ordsucun  7870  xp2nd  8068  2ndconst  8149  sexp2  8200  smoord  8411  tfrlem9  8431  tfrlem11  8434  oaass  8607  omordi  8612  omwordri  8618  odi  8625  oewordri  8639  nnawordi  8668  nnmordi  8678  coflton  8718  dom2lem  9057  fundmen  9097  sbthlem9  9152  mapen  9198  mapunen  9203  ssenen  9208  domfi  9242  mapfien  9437  inf3lem6  9671  ttrclselem2  9764  frind  9791  r1val1  9830  rankval3b  9873  numacn  10167  infxpabs  10328  infxp  10331  cfsmolem  10387  infpssrlem4  10423  fin23lem27  10445  isf34lem4  10494  hsmexlem2  10544  axdc3lem2  10568  axdc3lem4  10570  iundom2g  10663  gchen1  10749  fpwwe2lem6  10760  fpwwe2lem10  10764  fpwwe2lem11  10765  prlem936  11171  muladd  11787  leord1  11883  eqord1  11884  ltord2  11885  leord2  11886  eqord2  11887  divadddiv  12072  ltmul12a  12213  lemul12b  12214  fimaxre  12301  supadd  12325  supmullem1  12327  cju  12356  zextlt  12813  zmax  13112  xrre  13339  supxr  13483  ixxdisj  13531  iooshf  13597  icodisj  13647  ioojoin  13654  iccshftr  13657  iccshftl  13659  iccdil  13661  icccntr  13663  iccf1o  13667  fzaddel  13732  fzsubel  13734  modadd1  14088  modmul1  14107  seqcaopr  14222  expsub  14293  expmordi  14350  sqlecan  14393  facndiv  14473  hashss  14594  hashfacen  14640  hashf1lem1  14641  fi1uzind  14693  brfi1indALT  14696  ccatpfx  14892  swrdccatfn  14915  swrdccatin2  14920  2cshwcshw  15018  resqrex  15460  fprodeq0  16186  lcmdvds  16827  hashdvds  16996  eulerthlem2  17003  pceu  17068  pcqcl  17078  infpnlem1  17132  4sqlem11  17177  ramcl  17251  prmgaplem5  17277  imasvscafn  17759  invfun  17989  initoeu2lem2  18240  catcisolem  18335  funcestrcsetclem8  18371  fullestrcsetc  18375  embedsetcestrclem  18381  funcsetcestrclem8  18386  fullsetcestrc  18390  prfcl  18427  prf1st  18428  prf2nd  18429  1st2ndprf  18430  curfuncf  18462  ipodrsfi  18763  mgmhmpropd  18937  subsubmgm  18949  mhmpropd  19037  subsubm  19062  pwsdiagmhm  19077  frmdgsum  19108  grplcan  19261  grplmulf1o  19273  grpraddf1o  19274  dfgrp3lem  19298  mulgsubcl  19348  subsubg  19410  eqger  19440  qus0subgadd  19464  resghm  19496  conjghm  19513  orbsta  19578  psgnunilem2  19760  odmulg  19821  sylow2a  19884  sylow3lem1  19892  lsmssv  19908  pj1ghm  19968  frgpup1  20040  ghmplusg  20111  subsubrng  20866  subsubrg  20901  srhmsubc  20983  issrngd  21163  lmhmco  21369  lmhmf1o  21372  lmhmima  21373  lmhmpreima  21374  reslmhm  21378  pwsdiaglmhm  21383  pwssplit2  21386  pwssplit3  21387  pj1lmhm  21426  lspdisj  21454  rngqiprngghmlem2  21635  rngqiprngghm  21646  prmirred  21835  cygznlem3  21930  frlmsslsp  22157  frlmlbs  22158  frlmup1  22159  lindsenlbs  22212  issubassa2  22255  psrbagconf1o  22292  psrgrp  22319  evlslem2  22443  evlslem1  22446  evlsvvval  22457  ply1sclf1  22663  mamuass  22772  dmatmul  22867  dmatsubcl  22868  dmatmulcl  22870  dmatcrng  22872  scmatcrng  22891  mdetunilem9  22990  pm2mpghm  23189  fvmptnn04ifb  23224  toponmre  23466  neiptopreu  23506  ordtbas  23565  txcls  23978  txlm  24022  qtoptop2  24073  qtoprest  24091  kqt0lem  24110  ptuncnv  24181  fmfnfmlem4  24331  alexsubALTlem2  24422  tgpmulg  24467  blin  24795  xmeter  24807  xmetresbl  24811  dscmet  24946  nmdvr  25044  metnrmlem3  25236  icccvx  25326  bndth  25334  htpycc  25356  pcohtpylem  25395  pi1blem  25415  lmmbrf  25638  iscfil2  25642  iscau4  25655  minveclem7  25811  elovolm  25851  dyaddisjlem  25971  ismbfd  26015  itg1mulc  26080  dvlip  26368  dvcvx  26395  plypf1  26586  eff1olem  26933  logccv  27048  lawcos  27201  leibpilem1  27325  sqff1o  27566  dvdsppwf1o  27570  dvdsflf1o  27571  fsumdvdsmul  27579  sgmmul  27585  fsumvma  27597  bposlem6  27673  lgsdchr  27739  rpvmasum2  27896  pntpbnd1  27970  ostthlem1  28011  ltsres  28076  nodenselem5  28102  nodenselem6  28103  nodense  28106  addsproplem2  28413  mulsuniflem  28592  mulsunif2lem  28612  precsexlem9  28658  precsexlem10  28659  precsexlem11  28660  om2noseqlt2  28743  om2noseqf1o  28744  z12sge0  28926  elreno2  28938  tgbtwntriv2  29007  ercgrg  29037  hlpasch  29291  colinearalglem4  29544  axlowdimlem15  29591  axcontlem7  29605  axcontlem8  29606  axcontlem10  29608  usgr1v  29894  pthdivtx  30369  clwwlkn1loopb  30691  grpolcan  31189  nvmf  31304  sspmval  31392  nmosetre  31423  minvecolem7  31542  hiassdi  31750  shscli  31976  fh1  32277  fh2  32278  cm2j  32279  chscllem2  32297  spansncvi  32311  5oalem2  32314  adjsym  32492  nmopsetretALT  32522  nmfnsetre  32536  cnvadj  32551  cnvunop  32577  unoplin  32579  hmoplin  32601  lnopmi  32659  hmops  32679  hmopm  32680  nmcexi  32685  adjlnop  32745  adjmul  32751  adjadd  32752  opsqrlem1  32799  mdsl0  32969  ssmd2  32971  mdexchi  32994  superpos  33013  chrelat2i  33024  atcvatlem  33044  atcvati  33045  chirredlem1  33049  chirredi  33053  atcvat3i  33055  atcvat4i  33056  mdsymlem3  33064  mdsymlem5  33066  cdj3lem2b  33096  ifnebib  33243  isoun  33392  xrge0infss  33448  1arithufdlem3  34182  extdg1id  34409  ddemeas  34980  fsum2dsub  35347  hgt750lemb  35396  bnj1145  35734  brlexod  36040  brr0d  36042  subfacp1lem3  36155  subfacp1lem5  36157  cvxpconn  36215  satfv1lem  36335  btwnconn1lem12  37078  colinbtwnle  37098  broutsideof2  37102  lineelsb2  37128  nadddilem2  37185  nadddilem4  37187  nn0prpwlem  37325  neibastop2lem  37363  tailfb  37380  onsuct0  37444  finxpreclem2  38581  poimirlem4  38810  poimirlem26  38832  poimirlem27  38833  poimirlem31  38837  heicant  38841  mblfinlem2  38844  mblfinlem3  38845  ismblfin  38847  ftc1anclem5  38883  ftc1anclem6  38884  ftc1anc  38887  sdclem1  38943  seqpo  38947  sstotbnd  38975  cntotbnd  38996  ismtycnv  39002  ismtyres  39008  heibor  39021  exidreslem  39077  ghomdiv  39092  grpokerinj  39093  rngohomco  39174  rngoisoco  39182  idlsubcl  39223  divrngidl  39228  ispridl2  39238  ispridlc  39270  riotasv3d  40283  omllaw3  40568  omlfh1N  40581  hlrelat2  40726  cvratlem  40744  cvrat  40745  cvrat3  40765  cvrat4  40766  ps-2  40801  elpaddn0  41123  paddss12  41142  pmodlem2  41170  cdleme0cq  41538  cdlemeg49lebilem  41862  cdleme50eq  41864  tendoeq2  42097  tendoex  42298  diameetN  42379  diainN  42380  dvhopN  42439  djajN  42460  dihmeetcl  42668  mapdheq2  43052  3factsumint1  43337  imacrhmcl  43847  psrmnd  43873  evlselvlem  43882  fsuppind  43884  0prjspn  43930  fphpdo  44090  pell1234qrne0  44126  pell14qrgt0  44132  pell1qrge1  44143  monotoddzzfi  44215  jm2.18  44261  wepwsolem  44315  dnnumch3  44320  dnwech  44321  kelac1  44331  kercvrlsm  44351  onov0suclim  44537  cantnfresb  44587  dssmapnvod  45281  gsumws3  45457  gsumws4  45458  mnuprdlem1  45517  mnuprdlem2  45518  traxext  46231  modelac8prim  46246  cncmpmax  46323  fiiuncl  46356  choicefi  46487  mullimc  46901  mullimcf  46908  idlimc  46911  limclner  46934  climleltrp  46959  limsupub  46987  climuzlem  47026  climliminflimsup2  47092  xlimbr  47110  xlimxrre  47114  dfxlim2v  47130  fperdvper  47202  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnprodlem1  47229  stoweidlem27  47310  stoweidlem48  47331  fourierdlem42  47432  fourierdlem63  47452  fourierdlem65  47454  dfsalgen2  47624  subsaliuncl  47641  sge0iunmptlemfi  47696  sge0rpcpnf  47704  iundjiun  47743  psmeasure  47754  ovnsubaddlem2  47854  hoidmvle  47883  ovolval4lem2  47933  smflimlem2  48055  smflimlem3  48056  smflimlem6  48059  smflimmpt  48093  fcoresf1  48412  icceuelpart  48791  gpgedgvtx0  49432  gpgedgvtx1  49433  srhmsubcALTV  49695  catprs  50456  thincciso2  50921  functermclem  50973  functermc  50974  fulltermc  50977