Theorem adantrl 722

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad2ant2l  752  ad2ant2rl  755  cases2ALT  1054  consensus  1058  3ad2antr2  1196  3ad2antr3  1197  po2ne  5542  opabssxpd  5665  frpoind  6293  ordelord  6332  f1un  6787  fvelima2  6879  f1cofveqaeqALT  7202  isocnv  7274  isores2  7277  f1oiso2  7296  offval  7629  ordsucun  7765  xp2nd  7964  2ndconst  8040  sexp2  8086  smoord  8295  tfrlem9  8314  tfrlem11  8317  oaass  8486  omordi  8491  omwordri  8497  odi  8504  oewordri  8518  nnawordi  8547  nnmordi  8557  coflton  8597  dom2lem  8929  fundmen  8968  sbthlem9  9023  mapen  9069  mapunen  9074  ssenen  9079  domfi  9113  mapfien  9311  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  20535  subsubrg  20570  srhmsubc  20652  issrngd  20827  lmhmco  21033  lmhmf1o  21036  lmhmima  21037  lmhmpreima  21038  reslmhm  21042  pwsdiaglmhm  21047  pwssplit2  21050  pwssplit3  21051  pj1lmhm  21090  lspdisj  21118  rngqiprngghmlem2  21281  rngqiprngghm  21292  prmirred  21449  cygznlem3  21544  frlmsslsp  21771  frlmlbs  21772  frlmup1  21773  issubassa2  21867  psrbagconf1o  21904  psrgrp  21931  evlslem2  22055  evlslem1  22058  evlsvvval  22069  ply1sclf1  22275  mamuass  22385  dmatmul  22480  dmatsubcl  22481  dmatmulcl  22483  dmatcrng  22485  scmatcrng  22504  mdetunilem9  22603  pm2mpghm  22799  fvmptnn04ifb  22834  toponmre  23076  neiptopreu  23116  ordtbas  23175  txcls  23587  txlm  23631  qtoptop2  23682  qtoprest  23700  kqt0lem  23719  ptuncnv  23790  fmfnfmlem4  23940  alexsubALTlem2  24031  tgpmulg  24076  blin  24404  xmeter  24416  xmetresbl  24420  dscmet  24555  nmdvr  24653  metnrmlem3  24845  icccvx  24935  bndth  24943  htpycc  24965  pcohtpylem  25004  pi1blem  25024  lmmbrf  25247  iscfil2  25251  iscau4  25264  minveclem7  25420  elovolm  25460  dyaddisjlem  25580  ismbfd  25624  itg1mulc  25689  dvlip  25978  dvcvx  26005  plypf1  26195  eff1olem  26530  logccv  26645  lawcos  26798  leibpilem1  26922  sqff1o  27163  dvdsppwf1o  27167  dvdsflf1o  27168  fsumdvdsmul  27176  sgmmul  27182  fsumvma  27194  bposlem6  27270  lgsdchr  27336  rpvmasum2  27493  pntpbnd1  27567  ostthlem1  27608  ltsres  27644  nodenselem5  27670  nodenselem6  27671  nodense  27674  addsproplem2  27980  mulsuniflem  28159  mulsunif2lem  28179  precsexlem9  28225  precsexlem10  28226  precsexlem11  28227  om2noseqlt2  28310  om2noseqf1o  28311  z12sge0  28493  elreno2  28505  tgbtwntriv2  28573  ercgrg  28603  hlpasch  28842  colinearalglem4  28996  axlowdimlem15  29043  axcontlem7  29057  axcontlem8  29058  axcontlem10  29060  usgr1v  29343  pthdivtx  29813  clwwlkn1loopb  30131  grpolcan  30619  nvmf  30734  sspmval  30822  nmosetre  30853  minvecolem7  30972  hiassdi  31180  shscli  31406  fh1  31707  fh2  31708  cm2j  31709  chscllem2  31727  spansncvi  31741  5oalem2  31744  adjsym  31922  nmopsetretALT  31952  nmfnsetre  31966  cnvadj  31981  cnvunop  32007  unoplin  32009  hmoplin  32031  lnopmi  32089  hmops  32109  hmopm  32110  nmcexi  32115  adjlnop  32175  adjmul  32181  adjadd  32182  opsqrlem1  32229  mdsl0  32399  ssmd2  32401  mdexchi  32424  superpos  32443  chrelat2i  32454  atcvatlem  32474  atcvati  32475  chirredlem1  32479  chirredi  32483  atcvat3i  32485  atcvat4i  32486  mdsymlem3  32494  mdsymlem5  32496  cdj3lem2b  32526  ifnebib  32637  isoun  32794  xrge0infss  32852  1arithufdlem3  33629  extdg1id  33850  ddemeas  34420  fsum2dsub  34791  hgt750lemb  34840  bnj1145  35175  subfacp1lem3  35410  subfacp1lem5  35412  cvxpconn  35470  satfv1lem  35590  btwnconn1lem12  36326  colinbtwnle  36346  broutsideof2  36350  lineelsb2  36376  nn0prpwlem  36550  neibastop2lem  36588  tailfb  36605  onsuct0  36669  finxpreclem2  37752  lindsenlbs  37982  poimirlem4  37991  poimirlem26  38013  poimirlem27  38014  poimirlem31  38018  heicant  38022  mblfinlem2  38025  mblfinlem3  38026  ismblfin  38028  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anc  38068  sdclem1  38110  seqpo  38114  sstotbnd  38142  cntotbnd  38163  ismtycnv  38169  ismtyres  38175  heibor  38188  exidreslem  38244  ghomdiv  38259  grpokerinj  38260  rngohomco  38341  rngoisoco  38349  idlsubcl  38390  divrngidl  38395  ispridl2  38405  ispridlc  38437  riotasv3d  39452  omllaw3  39737  omlfh1N  39750  hlrelat2  39895  cvratlem  39913  cvrat  39914  cvrat3  39934  cvrat4  39935  ps-2  39970  elpaddn0  40292  paddss12  40311  pmodlem2  40339  cdleme0cq  40707  cdlemeg49lebilem  41031  cdleme50eq  41033  tendoeq2  41266  tendoex  41467  diameetN  41548  diainN  41549  dvhopN  41608  djajN  41629  dihmeetcl  41837  mapdheq2  42221  3factsumint1  42506  imacrhmcl  43004  psrmnd  43029  evlselvlem  43038  fsuppind  43040  0prjspn  43078  fphpdo  43262  pell1234qrne0  43298  pell14qrgt0  43304  pell1qrge1  43315  monotoddzzfi  43387  jm2.18  43433  wepwsolem  43487  dnnumch3  43492  dnwech  43493  kelac1  43508  kercvrlsm  43528  onov0suclim  43719  cantnfresb  43769  dssmapnvod  44464  gsumws3  44640  gsumws4  44641  mnuprdlem1  44716  mnuprdlem2  44717  traxext  45421  modelac8prim  45436  cncmpmax  45480  fiiuncl  45513  choicefi  45646  mullimc  46061  mullimcf  46068  idlimc  46071  limclner  46094  climleltrp  46119  limsupub  46147  climuzlem  46186  climliminflimsup2  46252  xlimbr  46270  xlimxrre  46274  dfxlim2v  46290  fperdvper  46362  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnprodlem1  46389  stoweidlem27  46470  stoweidlem48  46491  fourierdlem42  46592  fourierdlem63  46612  fourierdlem65  46614  dfsalgen2  46784  subsaliuncl  46801  sge0iunmptlemfi  46856  sge0rpcpnf  46864  iundjiun  46903  psmeasure  46914  ovnsubaddlem2  47014  hoidmvle  47043  ovolval4lem2  47093  smflimlem2  47215  smflimlem3  47216  smflimlem6  47219  smflimmpt  47253  fcoresf1  47532  icceuelpart  47911  gpgedgvtx0  48552  gpgedgvtx1  48553  srhmsubcALTV  48816  catprs  49501  thincciso2  49945  functermclem  49997  functermc  49998  fulltermc  50001