Theorem adantrl 717

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad2ant2l  747  ad2ant2rl  750  cases2ALT  1049  consensus  1053  3ad2antr2  1191  3ad2antr3  1192  po2ne  5548  opabssxpd  5671  frpoind  6300  ordelord  6339  f1un  6794  fvelima2  6886  f1cofveqaeqALT  7206  isocnv  7278  isores2  7281  f1oiso2  7300  offval  7633  ordsucun  7769  xp2nd  7968  2ndconst  8044  sexp2  8089  smoord  8298  tfrlem9  8317  tfrlem11  8320  oaass  8489  omordi  8494  omwordri  8500  odi  8507  oewordri  8521  nnawordi  8550  nnmordi  8560  coflton  8600  dom2lem  8932  fundmen  8971  sbthlem9  9026  mapen  9072  mapunen  9077  ssenen  9082  domfi  9116  mapfien  9314  inf3lem6  9545  ttrclselem2  9638  frind  9665  r1val1  9701  rankval3b  9741  numacn  9962  infxpabs  10124  infxp  10127  cfsmolem  10183  infpssrlem4  10219  fin23lem27  10241  isf34lem4  10290  hsmexlem2  10340  axdc3lem2  10364  axdc3lem4  10366  iundom2g  10453  gchen1  10539  fpwwe2lem6  10550  fpwwe2lem10  10554  fpwwe2lem11  10555  prlem936  10961  muladd  11573  leord1  11668  eqord1  11669  ltord2  11670  leord2  11671  eqord2  11672  divadddiv  11861  ltmul12a  12002  lemul12b  12003  fimaxre  12091  supadd  12115  supmullem1  12117  cju  12146  zextlt  12594  zmax  12886  xrre  13112  supxr  13256  ixxdisj  13304  iooshf  13370  icodisj  13420  ioojoin  13427  iccshftr  13430  iccshftl  13432  iccdil  13434  icccntr  13436  iccf1o  13440  fzaddel  13503  fzsubel  13505  modadd1  13858  modmul1  13877  seqcaopr  13992  expsub  14063  expmordi  14120  sqlecan  14162  facndiv  14241  hashss  14362  hashfacen  14407  hashf1lem1  14408  fi1uzind  14460  brfi1indALT  14463  ccatpfx  14654  swrdccatfn  14677  swrdccatin2  14682  2cshwcshw  14778  resqrex  15203  fprodeq0  15931  lcmdvds  16568  hashdvds  16736  eulerthlem2  16743  pceu  16808  pcqcl  16818  infpnlem1  16872  4sqlem11  16917  ramcl  16991  prmgaplem5  17017  imasvscafn  17492  invfun  17722  initoeu2lem2  17973  catcisolem  18068  funcestrcsetclem8  18104  fullestrcsetc  18108  embedsetcestrclem  18114  funcsetcestrclem8  18119  fullsetcestrc  18123  prfcl  18160  prf1st  18161  prf2nd  18162  1st2ndprf  18163  curfuncf  18195  ipodrsfi  18496  mgmhmpropd  18657  subsubmgm  18669  mhmpropd  18751  subsubm  18775  pwsdiagmhm  18790  frmdgsum  18821  grplcan  18967  grplmulf1o  18980  grpraddf1o  18981  dfgrp3lem  19005  mulgsubcl  19055  subsubg  19116  eqger  19144  qus0subgadd  19165  resghm  19198  conjghm  19215  orbsta  19279  psgnunilem2  19461  odmulg  19522  sylow2a  19585  sylow3lem1  19593  lsmssv  19609  pj1ghm  19669  frgpup1  19741  ghmplusg  19812  subsubrng  20531  subsubrg  20566  srhmsubc  20648  issrngd  20823  lmhmco  21030  lmhmf1o  21033  lmhmima  21034  lmhmpreima  21035  reslmhm  21039  pwsdiaglmhm  21044  pwssplit2  21047  pwssplit3  21048  pj1lmhm  21087  lspdisj  21115  rngqiprngghmlem2  21278  rngqiprngghm  21289  prmirred  21464  cygznlem3  21559  frlmsslsp  21786  frlmlbs  21787  frlmup1  21788  issubassa2  21882  psrbagconf1o  21919  psrgrp  21945  evlslem2  22067  evlslem1  22070  evlsvvval  22081  ply1sclf1  22264  mamuass  22377  dmatmul  22472  dmatsubcl  22473  dmatmulcl  22475  dmatcrng  22477  scmatcrng  22496  mdetunilem9  22595  pm2mpghm  22791  fvmptnn04ifb  22826  toponmre  23068  neiptopreu  23108  ordtbas  23167  txcls  23579  txlm  23623  qtoptop2  23674  qtoprest  23692  kqt0lem  23711  ptuncnv  23782  fmfnfmlem4  23932  alexsubALTlem2  24023  tgpmulg  24068  blin  24396  xmeter  24408  xmetresbl  24412  dscmet  24547  nmdvr  24645  metnrmlem3  24837  icccvx  24927  bndth  24935  htpycc  24957  pcohtpylem  24996  pi1blem  25016  lmmbrf  25239  iscfil2  25243  iscau4  25256  minveclem7  25412  elovolm  25452  dyaddisjlem  25572  ismbfd  25616  itg1mulc  25681  dvlip  25970  dvcvx  25997  plypf1  26187  eff1olem  26525  logccv  26640  lawcos  26793  leibpilem1  26917  sqff1o  27159  dvdsppwf1o  27163  dvdsflf1o  27164  fsumdvdsmul  27172  sgmmul  27178  fsumvma  27190  bposlem6  27266  lgsdchr  27332  rpvmasum2  27489  pntpbnd1  27563  ostthlem1  27604  ltsres  27640  nodenselem5  27666  nodenselem6  27667  nodense  27670  addsproplem2  27976  mulsuniflem  28155  mulsunif2lem  28175  precsexlem9  28221  precsexlem10  28222  precsexlem11  28223  om2noseqlt2  28306  om2noseqf1o  28307  z12sge0  28489  elreno2  28501  tgbtwntriv2  28569  ercgrg  28599  hlpasch  28838  colinearalglem4  28992  axlowdimlem15  29039  axcontlem7  29053  axcontlem8  29054  axcontlem10  29056  usgr1v  29339  pthdivtx  29810  clwwlkn1loopb  30128  grpolcan  30616  nvmf  30731  sspmval  30819  nmosetre  30850  minvecolem7  30969  hiassdi  31177  shscli  31403  fh1  31704  fh2  31705  cm2j  31706  chscllem2  31724  spansncvi  31738  5oalem2  31741  adjsym  31919  nmopsetretALT  31949  nmfnsetre  31963  cnvadj  31978  cnvunop  32004  unoplin  32006  hmoplin  32028  lnopmi  32086  hmops  32106  hmopm  32107  nmcexi  32112  adjlnop  32172  adjmul  32178  adjadd  32179  opsqrlem1  32226  mdsl0  32396  ssmd2  32398  mdexchi  32421  superpos  32440  chrelat2i  32451  atcvatlem  32471  atcvati  32472  chirredlem1  32476  chirredi  32480  atcvat3i  32482  atcvat4i  32483  mdsymlem3  32491  mdsymlem5  32493  cdj3lem2b  32523  ifnebib  32634  isoun  32790  xrge0infss  32848  1arithufdlem3  33621  extdg1id  33826  ddemeas  34396  fsum2dsub  34767  hgt750lemb  34816  bnj1145  35151  subfacp1lem3  35380  subfacp1lem5  35382  cvxpconn  35440  satfv1lem  35560  btwnconn1lem12  36296  colinbtwnle  36316  broutsideof2  36320  lineelsb2  36346  nn0prpwlem  36520  neibastop2lem  36558  tailfb  36575  onsuct0  36639  finxpreclem2  37720  lindsenlbs  37950  poimirlem4  37959  poimirlem26  37981  poimirlem27  37982  poimirlem31  37986  heicant  37990  mblfinlem2  37993  mblfinlem3  37994  ismblfin  37996  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anc  38036  sdclem1  38078  seqpo  38082  sstotbnd  38110  cntotbnd  38131  ismtycnv  38137  ismtyres  38143  heibor  38156  exidreslem  38212  ghomdiv  38227  grpokerinj  38228  rngohomco  38309  rngoisoco  38317  idlsubcl  38358  divrngidl  38363  ispridl2  38373  ispridlc  38405  riotasv3d  39420  omllaw3  39705  omlfh1N  39718  hlrelat2  39863  cvratlem  39881  cvrat  39882  cvrat3  39902  cvrat4  39903  ps-2  39938  elpaddn0  40260  paddss12  40279  pmodlem2  40307  cdleme0cq  40675  cdlemeg49lebilem  40999  cdleme50eq  41001  tendoeq2  41234  tendoex  41435  diameetN  41516  diainN  41517  dvhopN  41576  djajN  41597  dihmeetcl  41805  mapdheq2  42189  3factsumint1  42474  imacrhmcl  42973  psrmnd  43002  evlselvlem  43033  fsuppind  43037  0prjspn  43075  fphpdo  43263  pell1234qrne0  43299  pell14qrgt0  43305  pell1qrge1  43316  monotoddzzfi  43388  jm2.18  43434  wepwsolem  43488  dnnumch3  43493  dnwech  43494  kelac1  43509  kercvrlsm  43529  onov0suclim  43720  cantnfresb  43770  dssmapnvod  44465  gsumws3  44641  gsumws4  44642  mnuprdlem1  44717  mnuprdlem2  44718  traxext  45422  modelac8prim  45437  cncmpmax  45481  fiiuncl  45514  choicefi  45647  mullimc  46064  mullimcf  46071  idlimc  46074  limclner  46097  climleltrp  46122  limsupub  46150  climuzlem  46189  climliminflimsup2  46255  xlimbr  46273  xlimxrre  46277  dfxlim2v  46293  fperdvper  46365  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnprodlem1  46392  stoweidlem27  46473  stoweidlem48  46494  fourierdlem42  46595  fourierdlem63  46615  fourierdlem65  46617  dfsalgen2  46787  subsaliuncl  46804  sge0iunmptlemfi  46859  sge0rpcpnf  46867  iundjiun  46906  psmeasure  46917  ovnsubaddlem2  47017  hoidmvle  47046  ovolval4lem2  47096  smflimlem2  47218  smflimlem3  47219  smflimlem6  47222  smflimmpt  47256  fcoresf1  47529  icceuelpart  47908  gpgedgvtx0  48549  gpgedgvtx1  48550  srhmsubcALTV  48813  catprs  49498  thincciso2  49942  functermclem  49994  functermc  49995  fulltermc  49998