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  5579  opabssxpd  5702  frpoind  6340  ordelord  6379  f1un  6838  fvelima2  6930  f1cofveqaeqALT  7255  isocnv  7331  isores2  7334  f1oiso2  7353  offval  7687  ordsucun  7821  xp2nd  8019  2ndconst  8098  sexp2  8144  smoord  8354  tfrlem9  8374  tfrlem11  8377  oaass  8548  omordi  8553  omwordri  8559  odi  8566  oewordri  8580  nnawordi  8609  nnmordi  8619  coflton  8659  dom2lem  8998  fundmen  9038  sbthlem9  9093  mapen  9139  mapunen  9144  ssenen  9149  domfi  9183  mapfien  9378  inf3lem6  9612  ttrclselem2  9705  frind  9732  r1val1  9768  rankval3b  9808  numacn  10052  infxpabs  10213  infxp  10216  cfsmolem  10272  infpssrlem4  10308  fin23lem27  10330  isf34lem4  10379  hsmexlem2  10429  axdc3lem2  10453  axdc3lem4  10455  iundom2g  10548  gchen1  10634  fpwwe2lem6  10645  fpwwe2lem10  10649  fpwwe2lem11  10650  prlem936  11056  muladd  11670  leord1  11765  eqord1  11766  ltord2  11767  leord2  11768  eqord2  11769  divadddiv  11954  ltmul12a  12095  lemul12b  12096  fimaxre  12183  supadd  12207  supmullem1  12209  cju  12238  zextlt  12695  zmax  12994  xrre  13221  supxr  13365  ixxdisj  13413  iooshf  13479  icodisj  13529  ioojoin  13536  iccshftr  13539  iccshftl  13541  iccdil  13543  icccntr  13545  iccf1o  13549  fzaddel  13613  fzsubel  13615  modadd1  13969  modmul1  13988  seqcaopr  14103  expsub  14174  expmordi  14231  sqlecan  14273  facndiv  14352  hashss  14473  hashfacen  14519  hashf1lem1  14520  fi1uzind  14572  brfi1indALT  14575  ccatpfx  14770  swrdccatfn  14793  swrdccatin2  14798  2cshwcshw  14896  resqrex  15337  fprodeq0  16062  lcmdvds  16698  hashdvds  16866  eulerthlem2  16873  pceu  16938  pcqcl  16948  infpnlem1  17002  4sqlem11  17047  ramcl  17121  prmgaplem5  17147  imasvscafn  17623  invfun  17853  initoeu2lem2  18104  catcisolem  18199  funcestrcsetclem8  18235  fullestrcsetc  18239  embedsetcestrclem  18245  funcsetcestrclem8  18250  fullsetcestrc  18254  prfcl  18291  prf1st  18292  prf2nd  18293  1st2ndprf  18294  curfuncf  18326  ipodrsfi  18627  mgmhmpropd  18800  subsubmgm  18812  mhmpropd  18900  subsubm  18925  pwsdiagmhm  18940  frmdgsum  18971  grplcan  19124  grplmulf1o  19136  grpraddf1o  19137  dfgrp3lem  19161  mulgsubcl  19211  subsubg  19273  eqger  19303  qus0subgadd  19327  resghm  19359  conjghm  19376  orbsta  19440  psgnunilem2  19622  odmulg  19683  sylow2a  19746  sylow3lem1  19754  lsmssv  19770  pj1ghm  19830  frgpup1  19902  ghmplusg  19973  subsubrng  20725  subsubrg  20760  srhmsubc  20842  issrngd  21021  lmhmco  21227  lmhmf1o  21230  lmhmima  21231  lmhmpreima  21232  reslmhm  21236  pwsdiaglmhm  21241  pwssplit2  21244  pwssplit3  21245  pj1lmhm  21284  lspdisj  21312  rngqiprngghmlem2  21491  rngqiprngghm  21502  prmirred  21687  cygznlem3  21782  frlmsslsp  22009  frlmlbs  22010  frlmup1  22011  lindsenlbs  22064  issubassa2  22107  psrbagconf1o  22144  psrgrp  22171  evlslem2  22295  evlslem1  22298  evlsvvval  22309  ply1sclf1  22515  mamuass  22624  dmatmul  22719  dmatsubcl  22720  dmatmulcl  22722  dmatcrng  22724  scmatcrng  22743  mdetunilem9  22842  pm2mpghm  23041  fvmptnn04ifb  23076  toponmre  23318  neiptopreu  23358  ordtbas  23417  txcls  23830  txlm  23874  qtoptop2  23925  qtoprest  23943  kqt0lem  23962  ptuncnv  24033  fmfnfmlem4  24183  alexsubALTlem2  24274  tgpmulg  24319  blin  24647  xmeter  24659  xmetresbl  24663  dscmet  24798  nmdvr  24896  metnrmlem3  25088  icccvx  25178  bndth  25186  htpycc  25208  pcohtpylem  25247  pi1blem  25267  lmmbrf  25490  iscfil2  25494  iscau4  25507  minveclem7  25663  elovolm  25703  dyaddisjlem  25823  ismbfd  25867  itg1mulc  25932  dvlip  26220  dvcvx  26247  plypf1  26438  eff1olem  26785  logccv  26900  lawcos  27053  leibpilem1  27177  sqff1o  27418  dvdsppwf1o  27422  dvdsflf1o  27423  fsumdvdsmul  27431  sgmmul  27437  fsumvma  27449  bposlem6  27525  lgsdchr  27591  rpvmasum2  27748  pntpbnd1  27822  ostthlem1  27863  ltsres  27898  nodenselem5  27924  nodenselem6  27925  nodense  27928  addsproplem2  28235  mulsuniflem  28414  mulsunif2lem  28434  precsexlem9  28480  precsexlem10  28481  precsexlem11  28482  om2noseqlt2  28565  om2noseqf1o  28566  z12sge0  28748  elreno2  28760  tgbtwntriv2  28829  ercgrg  28859  hlpasch  29113  colinearalglem4  29366  axlowdimlem15  29413  axcontlem7  29427  axcontlem8  29428  axcontlem10  29430  usgr1v  29716  pthdivtx  30191  clwwlkn1loopb  30513  grpolcan  31011  nvmf  31126  sspmval  31214  nmosetre  31245  minvecolem7  31364  hiassdi  31572  shscli  31798  fh1  32099  fh2  32100  cm2j  32101  chscllem2  32119  spansncvi  32133  5oalem2  32136  adjsym  32314  nmopsetretALT  32344  nmfnsetre  32358  cnvadj  32373  cnvunop  32399  unoplin  32401  hmoplin  32423  lnopmi  32481  hmops  32501  hmopm  32502  nmcexi  32507  adjlnop  32567  adjmul  32573  adjadd  32574  opsqrlem1  32621  mdsl0  32791  ssmd2  32793  mdexchi  32816  superpos  32835  chrelat2i  32846  atcvatlem  32866  atcvati  32867  chirredlem1  32871  chirredi  32875  atcvat3i  32877  atcvat4i  32878  mdsymlem3  32886  mdsymlem5  32888  cdj3lem2b  32918  ifnebib  33024  isoun  33174  xrge0infss  33231  1arithufdlem3  33956  extdg1id  34176  ddemeas  34747  fsum2dsub  35115  hgt750lemb  35164  bnj1145  35502  subfacp1lem3  35761  subfacp1lem5  35763  cvxpconn  35821  satfv1lem  35941  btwnconn1lem12  36678  colinbtwnle  36698  broutsideof2  36702  lineelsb2  36728  nadddilem2  36801  nadddilem4  36803  nn0prpwlem  36941  neibastop2lem  36979  tailfb  36996  onsuct0  37060  finxpreclem2  38144  poimirlem4  38373  poimirlem26  38395  poimirlem27  38396  poimirlem31  38400  heicant  38404  mblfinlem2  38407  mblfinlem3  38408  ismblfin  38410  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anc  38450  sdclem1  38493  seqpo  38497  sstotbnd  38525  cntotbnd  38546  ismtycnv  38552  ismtyres  38558  heibor  38571  exidreslem  38627  ghomdiv  38642  grpokerinj  38643  rngohomco  38724  rngoisoco  38732  idlsubcl  38773  divrngidl  38778  ispridl2  38788  ispridlc  38820  riotasv3d  39833  omllaw3  40118  omlfh1N  40131  hlrelat2  40276  cvratlem  40294  cvrat  40295  cvrat3  40315  cvrat4  40316  ps-2  40351  elpaddn0  40673  paddss12  40692  pmodlem2  40720  cdleme0cq  41088  cdlemeg49lebilem  41412  cdleme50eq  41414  tendoeq2  41647  tendoex  41848  diameetN  41929  diainN  41930  dvhopN  41989  djajN  42010  dihmeetcl  42218  mapdheq2  42602  3factsumint1  42887  imacrhmcl  43402  psrmnd  43425  evlselvlem  43434  fsuppind  43436  0prjspn  43474  fphpdo  43658  pell1234qrne0  43694  pell14qrgt0  43700  pell1qrge1  43711  monotoddzzfi  43783  jm2.18  43829  wepwsolem  43883  dnnumch3  43888  dnwech  43889  kelac1  43904  kercvrlsm  43924  onov0suclim  44115  cantnfresb  44165  dssmapnvod  44860  gsumws3  45036  gsumws4  45037  mnuprdlem1  45096  mnuprdlem2  45097  traxext  45800  modelac8prim  45815  cncmpmax  45866  fiiuncl  45899  choicefi  46031  mullimc  46446  mullimcf  46453  idlimc  46456  limclner  46479  climleltrp  46504  limsupub  46532  climuzlem  46571  climliminflimsup2  46637  xlimbr  46655  xlimxrre  46659  dfxlim2v  46675  fperdvper  46747  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnprodlem1  46774  stoweidlem27  46855  stoweidlem48  46876  fourierdlem42  46977  fourierdlem63  46997  fourierdlem65  46999  dfsalgen2  47169  subsaliuncl  47186  sge0iunmptlemfi  47241  sge0rpcpnf  47249  iundjiun  47288  psmeasure  47299  ovnsubaddlem2  47399  hoidmvle  47428  ovolval4lem2  47478  smflimlem2  47600  smflimlem3  47601  smflimlem6  47604  smflimmpt  47638  fcoresf1  47957  icceuelpart  48336  gpgedgvtx0  48977  gpgedgvtx1  48978  srhmsubcALTV  49240  catprs  49937  thincciso2  50381  functermclem  50433  functermc  50434  fulltermc  50437