Theorem adantrl 715

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ad2ant2l  745  ad2ant2rl  748  cases2ALT  1048  consensus  1052  3ad2antr2  1190  3ad2antr3  1191  po2ne  5605  opabssxpd  5724  frpoind  6344  wfiOLD  6353  ordelord  6387  f1un  6854  f1cofveqaeqALT  7258  isocnv  7327  isores2  7330  f1oiso2  7349  offval  7679  ordsucun  7813  xp2nd  8008  2ndconst  8087  sexp2  8132  wfrdmclOLD  8317  smoord  8365  tfrlem9  8385  tfrlem11  8388  oaass  8561  omordi  8566  omwordri  8572  odi  8579  oewordri  8592  nnawordi  8621  nnmordi  8631  coflton  8670  dom2lem  8988  fundmen  9031  sbthlem9  9091  mapen  9141  mapunen  9146  ssenen  9151  domfi  9192  mapfien  9403  inf3lem6  9628  ttrclselem2  9721  frind  9745  r1val1  9781  rankval3b  9821  numacn  10044  infxpabs  10207  infxp  10210  cfsmolem  10265  infpssrlem4  10301  fin23lem27  10323  isf34lem4  10372  hsmexlem2  10422  axdc3lem2  10446  axdc3lem4  10448  iundom2g  10535  gchen1  10620  fpwwe2lem6  10631  fpwwe2lem10  10635  fpwwe2lem11  10636  prlem936  11042  muladd  11646  leord1  11741  eqord1  11742  ltord2  11743  leord2  11744  eqord2  11745  divadddiv  11929  ltmul12a  12070  lemul12b  12071  fimaxre  12158  supadd  12182  supmullem1  12184  cju  12208  zextlt  12636  zmax  12929  xrre  13148  supxr  13292  ixxdisj  13339  iooshf  13403  icodisj  13453  ioojoin  13460  iccshftr  13463  iccshftl  13465  iccdil  13467  icccntr  13469  iccf1o  13473  fzaddel  13535  fzsubel  13537  modadd1  13873  modmul1  13889  seqcaopr  14005  expsub  14076  expmordi  14132  sqlecan  14173  facndiv  14248  hashss  14369  hashfacen  14413  hashfacenOLD  14414  hashf1lem1  14415  hashf1lem1OLD  14416  fi1uzind  14458  brfi1indALT  14461  ccatpfx  14651  swrdccatfn  14674  swrdccatin2  14679  2cshwcshw  14776  resqrex  15197  fprodeq0  15919  lcmdvds  16545  hashdvds  16708  eulerthlem2  16715  pceu  16779  pcqcl  16789  infpnlem1  16843  4sqlem11  16888  ramcl  16962  prmgaplem5  16988  imasvscafn  17483  invfun  17711  initoeu2lem2  17965  catcisolem  18060  funcestrcsetclem8  18099  fullestrcsetc  18103  embedsetcestrclem  18109  funcsetcestrclem8  18114  fullsetcestrc  18118  prfcl  18155  prf1st  18156  prf2nd  18157  1st2ndprf  18158  curfuncf  18191  ipodrsfi  18492  mhmpropd  18678  subsubm  18697  pwsdiagmhm  18712  frmdgsum  18743  grplcan  18885  grplmulf1o  18897  dfgrp3lem  18921  mulgsubcl  18968  subsubg  19029  eqger  19058  qus0subgadd  19076  resghm  19108  conjghm  19123  orbsta  19177  psgnunilem2  19363  odmulg  19424  sylow2a  19487  sylow3lem1  19495  lsmssv  19511  pj1ghm  19571  frgpup1  19643  ghmplusg  19714  subsubrg  20345  issrngd  20469  lmhmco  20654  lmhmf1o  20657  lmhmima  20658  lmhmpreima  20659  reslmhm  20663  pwsdiaglmhm  20668  pwssplit2  20671  pwssplit3  20672  pj1lmhm  20711  lspdisj  20738  prmirred  21044  cygznlem3  21125  frlmsslsp  21351  frlmlbs  21352  frlmup1  21353  issubassa2  21446  psrbagconf1o  21489  psrbagconf1oOLD  21490  psrgrp  21517  evlslem2  21642  evlslem1  21645  ply1sclf1  21811  mamuass  21902  dmatmul  21999  dmatsubcl  22000  dmatmulcl  22002  dmatcrng  22004  scmatcrng  22023  mdetunilem9  22122  pm2mpghm  22318  fvmptnn04ifb  22353  toponmre  22597  neiptopreu  22637  ordtbas  22696  txcls  23108  txlm  23152  qtoptop2  23203  qtoprest  23221  kqt0lem  23240  ptuncnv  23311  fmfnfmlem4  23461  alexsubALTlem2  23552  tgpmulg  23597  blin  23927  xmeter  23939  xmetresbl  23943  dscmet  24081  nmdvr  24187  metnrmlem3  24377  icccvx  24466  bndth  24474  htpycc  24496  pcohtpylem  24535  pi1blem  24555  lmmbrf  24779  iscfil2  24783  iscau4  24796  minveclem7  24952  elovolm  24992  dyaddisjlem  25112  ismbfd  25156  itg1mulc  25222  dvlip  25510  dvcvx  25537  plypf1  25726  eff1olem  26057  logccv  26171  lawcos  26321  leibpilem1  26445  sqff1o  26686  dvdsppwf1o  26690  dvdsflf1o  26691  fsumdvdsmul  26699  sgmmul  26704  fsumvma  26716  bposlem6  26792  lgsdchr  26858  rpvmasum2  27015  pntpbnd1  27089  ostthlem1  27130  sltres  27165  nodenselem5  27191  nodenselem6  27192  nodense  27195  addsproplem2  27454  mulsuniflem  27604  precsexlem9  27661  precsexlem10  27662  precsexlem11  27663  tgbtwntriv2  27738  ercgrg  27768  hlpasch  28007  colinearalglem4  28167  axlowdimlem15  28214  axcontlem7  28228  axcontlem8  28229  axcontlem10  28231  usgr1v  28513  pthdivtx  28986  clwwlkn1loopb  29296  grpolcan  29783  nvmf  29898  sspmval  29986  nmosetre  30017  minvecolem7  30136  hiassdi  30344  shscli  30570  fh1  30871  fh2  30872  cm2j  30873  chscllem2  30891  spansncvi  30905  5oalem2  30908  adjsym  31086  nmopsetretALT  31116  nmfnsetre  31130  cnvadj  31145  cnvunop  31171  unoplin  31173  hmoplin  31195  lnopmi  31253  hmops  31273  hmopm  31274  nmcexi  31279  adjlnop  31339  adjmul  31345  adjadd  31346  opsqrlem1  31393  mdsl0  31563  ssmd2  31565  mdexchi  31588  superpos  31607  chrelat2i  31618  atcvatlem  31638  atcvati  31639  chirredlem1  31643  chirredi  31647  atcvat3i  31649  atcvat4i  31650  mdsymlem3  31658  mdsymlem5  31660  cdj3lem2b  31690  ifnebib  31781  isoun  31923  xrge0infss  31973  extdg1id  32742  ddemeas  33234  fsum2dsub  33619  hgt750lemb  33668  bnj1145  34004  subfacp1lem3  34173  subfacp1lem5  34175  satfv1lem  34353  btwnconn1lem12  35070  colinbtwnle  35090  broutsideof2  35094  lineelsb2  35120  nn0prpwlem  35207  neibastop2lem  35245  tailfb  35262  onsuct0  35326  finxpreclem2  36271  lindsenlbs  36483  poimirlem4  36492  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  heicant  36523  mblfinlem2  36526  mblfinlem3  36527  ismblfin  36529  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anc  36569  sdclem1  36611  seqpo  36615  sstotbnd  36643  cntotbnd  36664  ismtycnv  36670  ismtyres  36676  heibor  36689  exidreslem  36745  ghomdiv  36760  grpokerinj  36761  rngohomco  36842  rngoisoco  36850  idlsubcl  36891  divrngidl  36896  ispridl2  36906  ispridlc  36938  riotasv3d  37830  omllaw3  38115  omlfh1N  38128  hlrelat2  38274  cvratlem  38292  cvrat  38293  cvrat3  38313  cvrat4  38314  ps-2  38349  elpaddn0  38671  paddss12  38690  pmodlem2  38718  cdleme0cq  39086  cdlemeg49lebilem  39410  cdleme50eq  39412  tendoeq2  39645  tendoex  39846  diameetN  39927  diainN  39928  dvhopN  39987  djajN  40008  dihmeetcl  40216  mapdheq2  40600  3factsumint1  40886  metakunt16  41000  imacrhmcl  41089  evlsvvval  41135  evlselvlem  41158  fsuppind  41162  0prjspn  41370  fphpdo  41555  pell1234qrne0  41591  pell14qrgt0  41597  pell1qrge1  41608  monotoddzzfi  41681  jm2.18  41727  wepwsolem  41784  dnnumch3  41789  dnwech  41790  kelac1  41805  kercvrlsm  41825  onov0suclim  42024  cantnfresb  42074  dssmapnvod  42771  gsumws3  42948  gsumws4  42949  mnuprdlem1  43031  mnuprdlem2  43032  cncmpmax  43716  fiiuncl  43752  choicefi  43899  fvelima2  43964  mullimc  44332  mullimcf  44339  idlimc  44342  limclner  44367  climleltrp  44392  limsupub  44420  climuzlem  44459  climliminflimsup2  44525  xlimbr  44543  xlimxrre  44547  dfxlim2v  44563  fperdvper  44635  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnprodlem1  44662  stoweidlem27  44743  stoweidlem48  44764  fourierdlem42  44865  fourierdlem63  44885  fourierdlem65  44887  dfsalgen2  45057  subsaliuncl  45074  sge0iunmptlemfi  45129  sge0rpcpnf  45137  iundjiun  45176  psmeasure  45187  ovnsubaddlem2  45287  hoidmvle  45316  ovolval4lem2  45366  smflimlem2  45488  smflimlem3  45489  smflimlem6  45492  smflimmpt  45526  fcoresf1  45779  icceuelpart  46104  mgmhmpropd  46555  subsubmgm  46567  subsubrng  46742  rngqiprngghmlem2  46773  rngqiprngghm  46784  srhmsubc  46974  srhmsubcALTV  46992  catprs  47631