Theorem adantrl 728

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 489	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 604	1 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad2ant2l  758  ad2ant2rl  761  cases2ALT  1062  consensus  1066  3ad2antr2  1206  3ad2antr3  1207  po2ne  5583  opabssxpd  5706  frpoind  6341  ordelord  6380  f1un  6839  fvelima2  6931  f1cofveqaeqALT  7254  isocnv  7326  isores2  7329  f1oiso2  7348  offval  7681  ordsucun  7817  xp2nd  8015  2ndconst  8092  sexp2  8138  smoord  8348  tfrlem9  8368  tfrlem11  8371  oaass  8542  omordi  8547  omwordri  8553  odi  8560  oewordri  8574  nnawordi  8603  nnmordi  8613  coflton  8653  dom2lem  8985  fundmen  9024  sbthlem9  9079  mapen  9125  mapunen  9130  ssenen  9135  domfi  9169  mapfien  9364  inf3lem6  9598  ttrclselem2  9691  frind  9718  r1val1  9754  rankval3b  9794  numacn  10029  infxpabs  10190  infxp  10193  cfsmolem  10250  infpssrlem4  10286  fin23lem27  10308  isf34lem4  10357  hsmexlem2  10407  axdc3lem2  10431  axdc3lem4  10433  iundom2g  10520  gchen1  10606  fpwwe2lem6  10617  fpwwe2lem10  10621  fpwwe2lem11  10622  prlem936  11028  muladd  11642  leord1  11737  eqord1  11738  ltord2  11739  leord2  11740  eqord2  11741  divadddiv  11926  ltmul12a  12067  lemul12b  12068  fimaxre  12155  supadd  12179  supmullem1  12181  cju  12210  zextlt  12666  zmax  12965  xrre  13191  supxr  13335  ixxdisj  13383  iooshf  13449  icodisj  13499  ioojoin  13506  iccshftr  13509  iccshftl  13511  iccdil  13513  icccntr  13515  iccf1o  13519  fzaddel  13582  fzsubel  13584  modadd1  13937  modmul1  13956  seqcaopr  14071  expsub  14142  expmordi  14199  sqlecan  14241  facndiv  14320  hashss  14441  hashfacen  14487  hashf1lem1  14488  fi1uzind  14540  brfi1indALT  14543  ccatpfx  14734  swrdccatfn  14757  swrdccatin2  14762  2cshwcshw  14858  resqrex  15297  fprodeq0  16025  lcmdvds  16662  hashdvds  16830  eulerthlem2  16837  pceu  16902  pcqcl  16912  infpnlem1  16966  4sqlem11  17011  ramcl  17085  prmgaplem5  17111  imasvscafn  17587  invfun  17817  initoeu2lem2  18068  catcisolem  18163  funcestrcsetclem8  18199  fullestrcsetc  18203  embedsetcestrclem  18209  funcsetcestrclem8  18214  fullsetcestrc  18218  prfcl  18255  prf1st  18256  prf2nd  18257  1st2ndprf  18258  curfuncf  18290  ipodrsfi  18591  mgmhmpropd  18752  subsubmgm  18764  mhmpropd  18846  subsubm  18871  pwsdiagmhm  18886  frmdgsum  18917  grplcan  19063  grplmulf1o  19075  grpraddf1o  19076  dfgrp3lem  19100  mulgsubcl  19150  subsubg  19212  eqger  19242  qus0subgadd  19266  resghm  19298  conjghm  19315  orbsta  19379  psgnunilem2  19561  odmulg  19622  sylow2a  19685  sylow3lem1  19693  lsmssv  19709  pj1ghm  19769  frgpup1  19841  ghmplusg  19912  subsubrng  20644  subsubrg  20679  srhmsubc  20761  issrngd  20932  lmhmco  21138  lmhmf1o  21141  lmhmima  21142  lmhmpreima  21143  reslmhm  21147  pwsdiaglmhm  21152  pwssplit2  21155  pwssplit3  21156  pj1lmhm  21195  lspdisj  21223  rngqiprngghmlem2  21395  rngqiprngghm  21406  prmirred  21589  cygznlem3  21684  frlmsslsp  21911  frlmlbs  21912  frlmup1  21913  issubassa2  22007  psrbagconf1o  22044  psrgrp  22071  evlslem2  22195  evlslem1  22198  evlsvvval  22209  ply1sclf1  22415  mamuass  22524  dmatmul  22619  dmatsubcl  22620  dmatmulcl  22622  dmatcrng  22624  scmatcrng  22643  mdetunilem9  22742  pm2mpghm  22938  fvmptnn04ifb  22973  toponmre  23215  neiptopreu  23255  ordtbas  23314  txcls  23726  txlm  23770  qtoptop2  23821  qtoprest  23839  kqt0lem  23858  ptuncnv  23929  fmfnfmlem4  24079  alexsubALTlem2  24170  tgpmulg  24215  blin  24543  xmeter  24555  xmetresbl  24559  dscmet  24694  nmdvr  24792  metnrmlem3  24984  icccvx  25074  bndth  25082  htpycc  25104  pcohtpylem  25143  pi1blem  25163  lmmbrf  25386  iscfil2  25390  iscau4  25403  minveclem7  25559  elovolm  25599  dyaddisjlem  25719  ismbfd  25763  itg1mulc  25828  dvlip  26117  dvcvx  26144  plypf1  26334  eff1olem  26675  logccv  26790  lawcos  26943  leibpilem1  27067  sqff1o  27308  dvdsppwf1o  27312  dvdsflf1o  27313  fsumdvdsmul  27321  sgmmul  27327  fsumvma  27339  bposlem6  27415  lgsdchr  27481  rpvmasum2  27638  pntpbnd1  27712  ostthlem1  27753  ltsres  27788  nodenselem5  27814  nodenselem6  27815  nodense  27818  addsproplem2  28125  mulsuniflem  28304  mulsunif2lem  28324  precsexlem9  28370  precsexlem10  28371  precsexlem11  28372  om2noseqlt2  28455  om2noseqf1o  28456  z12sge0  28638  elreno2  28650  tgbtwntriv2  28718  ercgrg  28748  hlpasch  28993  colinearalglem4  29196  axlowdimlem15  29243  axcontlem7  29257  axcontlem8  29258  axcontlem10  29260  usgr1v  29543  pthdivtx  30013  clwwlkn1loopb  30331  grpolcan  30819  nvmf  30934  sspmval  31022  nmosetre  31053  minvecolem7  31172  hiassdi  31380  shscli  31606  fh1  31907  fh2  31908  cm2j  31909  chscllem2  31927  spansncvi  31941  5oalem2  31944  adjsym  32122  nmopsetretALT  32152  nmfnsetre  32166  cnvadj  32181  cnvunop  32207  unoplin  32209  hmoplin  32231  lnopmi  32289  hmops  32309  hmopm  32310  nmcexi  32315  adjlnop  32375  adjmul  32381  adjadd  32382  opsqrlem1  32429  mdsl0  32599  ssmd2  32601  mdexchi  32624  superpos  32643  chrelat2i  32654  atcvatlem  32674  atcvati  32675  chirredlem1  32679  chirredi  32683  atcvat3i  32685  atcvat4i  32686  mdsymlem3  32694  mdsymlem5  32696  cdj3lem2b  32726  ifnebib  32832  isoun  32984  xrge0infss  33042  1arithufdlem3  33777  extdg1id  33997  ddemeas  34567  fsum2dsub  34935  hgt750lemb  34984  bnj1145  35322  subfacp1lem3  35569  subfacp1lem5  35571  cvxpconn  35629  satfv1lem  35749  btwnconn1lem12  36485  colinbtwnle  36505  broutsideof2  36509  lineelsb2  36535  nn0prpwlem  36718  neibastop2lem  36756  tailfb  36773  onsuct0  36837  finxpreclem2  37919  lindsenlbs  38149  poimirlem4  38158  poimirlem26  38180  poimirlem27  38181  poimirlem31  38185  heicant  38189  mblfinlem2  38192  mblfinlem3  38193  ismblfin  38195  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anc  38235  sdclem1  38277  seqpo  38281  sstotbnd  38309  cntotbnd  38330  ismtycnv  38336  ismtyres  38342  heibor  38355  exidreslem  38411  ghomdiv  38426  grpokerinj  38427  rngohomco  38508  rngoisoco  38516  idlsubcl  38557  divrngidl  38562  ispridl2  38572  ispridlc  38604  riotasv3d  39619  omllaw3  39904  omlfh1N  39917  hlrelat2  40062  cvratlem  40080  cvrat  40081  cvrat3  40101  cvrat4  40102  ps-2  40137  elpaddn0  40459  paddss12  40478  pmodlem2  40506  cdleme0cq  40874  cdlemeg49lebilem  41198  cdleme50eq  41200  tendoeq2  41433  tendoex  41634  diameetN  41715  diainN  41716  dvhopN  41775  djajN  41796  dihmeetcl  42004  mapdheq2  42388  3factsumint1  42673  imacrhmcl  43173  psrmnd  43198  evlselvlem  43207  fsuppind  43209  0prjspn  43247  fphpdo  43431  pell1234qrne0  43467  pell14qrgt0  43473  pell1qrge1  43484  monotoddzzfi  43556  jm2.18  43602  wepwsolem  43656  dnnumch3  43661  dnwech  43662  kelac1  43677  kercvrlsm  43697  onov0suclim  43888  cantnfresb  43938  dssmapnvod  44633  gsumws3  44809  gsumws4  44810  mnuprdlem1  44869  mnuprdlem2  44870  traxext  45573  modelac8prim  45588  cncmpmax  45639  fiiuncl  45672  choicefi  45804  mullimc  46219  mullimcf  46226  idlimc  46229  limclner  46252  climleltrp  46277  limsupub  46305  climuzlem  46344  climliminflimsup2  46410  xlimbr  46428  xlimxrre  46432  dfxlim2v  46448  fperdvper  46520  ioodvbdlimc1lem2  46533  ioodvbdlimc2lem  46535  dvnprodlem1  46547  stoweidlem27  46628  stoweidlem48  46649  fourierdlem42  46750  fourierdlem63  46770  fourierdlem65  46772  dfsalgen2  46942  subsaliuncl  46959  sge0iunmptlemfi  47014  sge0rpcpnf  47022  iundjiun  47061  psmeasure  47072  ovnsubaddlem2  47172  hoidmvle  47201  ovolval4lem2  47251  smflimlem2  47373  smflimlem3  47374  smflimlem6  47377  smflimmpt  47411  fcoresf1  47690  icceuelpart  48069  gpgedgvtx0  48710  gpgedgvtx1  48711  srhmsubcALTV  48974  catprs  49669  thincciso2  50113  functermclem  50165  functermc  50166  fulltermc  50169