Theorem adantrl 716

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 593	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  746  ad2ant2rl  749  cases2ALT  1048  consensus  1052  3ad2antr2  1190  3ad2antr3  1191  po2ne  5548  opabssxpd  5671  frpoind  6300  ordelord  6339  f1un  6794  fvelima2  6886  f1cofveqaeqALT  7204  isocnv  7276  isores2  7279  f1oiso2  7298  offval  7631  ordsucun  7767  xp2nd  7966  2ndconst  8043  sexp2  8088  smoord  8297  tfrlem9  8316  tfrlem11  8319  oaass  8488  omordi  8493  omwordri  8499  odi  8506  oewordri  8520  nnawordi  8549  nnmordi  8559  coflton  8599  dom2lem  8929  fundmen  8968  sbthlem9  9023  mapen  9069  mapunen  9074  ssenen  9079  domfi  9113  mapfien  9311  inf3lem6  9542  ttrclselem2  9635  frind  9662  r1val1  9698  rankval3b  9738  numacn  9959  infxpabs  10121  infxp  10124  cfsmolem  10180  infpssrlem4  10216  fin23lem27  10238  isf34lem4  10287  hsmexlem2  10337  axdc3lem2  10361  axdc3lem4  10363  iundom2g  10450  gchen1  10536  fpwwe2lem6  10547  fpwwe2lem10  10551  fpwwe2lem11  10552  prlem936  10958  muladd  11569  leord1  11664  eqord1  11665  ltord2  11666  leord2  11667  eqord2  11668  divadddiv  11856  ltmul12a  11997  lemul12b  11998  fimaxre  12086  supadd  12110  supmullem1  12112  cju  12141  zextlt  12566  zmax  12858  xrre  13084  supxr  13228  ixxdisj  13276  iooshf  13342  icodisj  13392  ioojoin  13399  iccshftr  13402  iccshftl  13404  iccdil  13406  icccntr  13408  iccf1o  13412  fzaddel  13474  fzsubel  13476  modadd1  13828  modmul1  13847  seqcaopr  13962  expsub  14033  expmordi  14090  sqlecan  14132  facndiv  14211  hashss  14332  hashfacen  14377  hashf1lem1  14378  fi1uzind  14430  brfi1indALT  14433  ccatpfx  14624  swrdccatfn  14647  swrdccatin2  14652  2cshwcshw  14748  resqrex  15173  fprodeq0  15898  lcmdvds  16535  hashdvds  16702  eulerthlem2  16709  pceu  16774  pcqcl  16784  infpnlem1  16838  4sqlem11  16883  ramcl  16957  prmgaplem5  16983  imasvscafn  17458  invfun  17688  initoeu2lem2  17939  catcisolem  18034  funcestrcsetclem8  18070  fullestrcsetc  18074  embedsetcestrclem  18080  funcsetcestrclem8  18085  fullsetcestrc  18089  prfcl  18126  prf1st  18127  prf2nd  18128  1st2ndprf  18129  curfuncf  18161  ipodrsfi  18462  mgmhmpropd  18623  subsubmgm  18635  mhmpropd  18717  subsubm  18741  pwsdiagmhm  18756  frmdgsum  18787  grplcan  18930  grplmulf1o  18943  grpraddf1o  18944  dfgrp3lem  18968  mulgsubcl  19018  subsubg  19079  eqger  19107  qus0subgadd  19128  resghm  19161  conjghm  19178  orbsta  19242  psgnunilem2  19424  odmulg  19485  sylow2a  19548  sylow3lem1  19556  lsmssv  19572  pj1ghm  19632  frgpup1  19704  ghmplusg  19775  subsubrng  20496  subsubrg  20531  srhmsubc  20613  issrngd  20788  lmhmco  20995  lmhmf1o  20998  lmhmima  20999  lmhmpreima  21000  reslmhm  21004  pwsdiaglmhm  21009  pwssplit2  21012  pwssplit3  21013  pj1lmhm  21052  lspdisj  21080  rngqiprngghmlem2  21243  rngqiprngghm  21254  prmirred  21429  cygznlem3  21524  frlmsslsp  21751  frlmlbs  21752  frlmup1  21753  issubassa2  21848  psrbagconf1o  21885  psrgrp  21912  evlslem2  22034  evlslem1  22037  evlsvvval  22048  ply1sclf1  22231  mamuass  22346  dmatmul  22441  dmatsubcl  22442  dmatmulcl  22444  dmatcrng  22446  scmatcrng  22465  mdetunilem9  22564  pm2mpghm  22760  fvmptnn04ifb  22795  toponmre  23037  neiptopreu  23077  ordtbas  23136  txcls  23548  txlm  23592  qtoptop2  23643  qtoprest  23661  kqt0lem  23680  ptuncnv  23751  fmfnfmlem4  23901  alexsubALTlem2  23992  tgpmulg  24037  blin  24365  xmeter  24377  xmetresbl  24381  dscmet  24516  nmdvr  24614  metnrmlem3  24806  icccvx  24904  bndth  24913  htpycc  24935  pcohtpylem  24975  pi1blem  24995  lmmbrf  25218  iscfil2  25222  iscau4  25235  minveclem7  25391  elovolm  25432  dyaddisjlem  25552  ismbfd  25596  itg1mulc  25661  dvlip  25954  dvcvx  25981  plypf1  26173  eff1olem  26513  logccv  26628  lawcos  26782  leibpilem1  26906  sqff1o  27148  dvdsppwf1o  27152  dvdsflf1o  27153  fsumdvdsmul  27161  fsumdvdsmulOLD  27163  sgmmul  27168  fsumvma  27180  bposlem6  27256  lgsdchr  27322  rpvmasum2  27479  pntpbnd1  27553  ostthlem1  27594  ltsres  27630  nodenselem5  27656  nodenselem6  27657  nodense  27660  addsproplem2  27966  mulsuniflem  28145  mulsunif2lem  28165  precsexlem9  28211  precsexlem10  28212  precsexlem11  28213  om2noseqlt2  28296  om2noseqf1o  28297  z12sge0  28479  elreno2  28491  tgbtwntriv2  28559  ercgrg  28589  hlpasch  28828  colinearalglem4  28982  axlowdimlem15  29029  axcontlem7  29043  axcontlem8  29044  axcontlem10  29046  usgr1v  29329  pthdivtx  29800  clwwlkn1loopb  30118  grpolcan  30605  nvmf  30720  sspmval  30808  nmosetre  30839  minvecolem7  30958  hiassdi  31166  shscli  31392  fh1  31693  fh2  31694  cm2j  31695  chscllem2  31713  spansncvi  31727  5oalem2  31730  adjsym  31908  nmopsetretALT  31938  nmfnsetre  31952  cnvadj  31967  cnvunop  31993  unoplin  31995  hmoplin  32017  lnopmi  32075  hmops  32095  hmopm  32096  nmcexi  32101  adjlnop  32161  adjmul  32167  adjadd  32168  opsqrlem1  32215  mdsl0  32385  ssmd2  32387  mdexchi  32410  superpos  32429  chrelat2i  32440  atcvatlem  32460  atcvati  32461  chirredlem1  32465  chirredi  32469  atcvat3i  32471  atcvat4i  32472  mdsymlem3  32480  mdsymlem5  32482  cdj3lem2b  32512  ifnebib  32624  isoun  32781  xrge0infss  32840  1arithufdlem3  33627  extdg1id  33823  ddemeas  34393  fsum2dsub  34764  hgt750lemb  34813  bnj1145  35149  subfacp1lem3  35376  subfacp1lem5  35378  cvxpconn  35436  satfv1lem  35556  btwnconn1lem12  36292  colinbtwnle  36312  broutsideof2  36316  lineelsb2  36342  nn0prpwlem  36516  neibastop2lem  36554  tailfb  36571  onsuct0  36635  finxpreclem2  37595  lindsenlbs  37816  poimirlem4  37825  poimirlem26  37847  poimirlem27  37848  poimirlem31  37852  heicant  37856  mblfinlem2  37859  mblfinlem3  37860  ismblfin  37862  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anc  37902  sdclem1  37944  seqpo  37948  sstotbnd  37976  cntotbnd  37997  ismtycnv  38003  ismtyres  38009  heibor  38022  exidreslem  38078  ghomdiv  38093  grpokerinj  38094  rngohomco  38175  rngoisoco  38183  idlsubcl  38224  divrngidl  38229  ispridl2  38239  ispridlc  38271  riotasv3d  39220  omllaw3  39505  omlfh1N  39518  hlrelat2  39663  cvratlem  39681  cvrat  39682  cvrat3  39702  cvrat4  39703  ps-2  39738  elpaddn0  40060  paddss12  40079  pmodlem2  40107  cdleme0cq  40475  cdlemeg49lebilem  40799  cdleme50eq  40801  tendoeq2  41034  tendoex  41235  diameetN  41316  diainN  41317  dvhopN  41376  djajN  41397  dihmeetcl  41605  mapdheq2  41989  3factsumint1  42275  imacrhmcl  42769  psrmnd  42798  evlselvlem  42829  fsuppind  42833  0prjspn  42871  fphpdo  43059  pell1234qrne0  43095  pell14qrgt0  43101  pell1qrge1  43112  monotoddzzfi  43184  jm2.18  43230  wepwsolem  43284  dnnumch3  43289  dnwech  43290  kelac1  43305  kercvrlsm  43325  onov0suclim  43516  cantnfresb  43566  dssmapnvod  44261  gsumws3  44437  gsumws4  44438  mnuprdlem1  44513  mnuprdlem2  44514  traxext  45218  modelac8prim  45233  cncmpmax  45277  fiiuncl  45310  choicefi  45444  mullimc  45862  mullimcf  45869  idlimc  45872  limclner  45895  climleltrp  45920  limsupub  45948  climuzlem  45987  climliminflimsup2  46053  xlimbr  46071  xlimxrre  46075  dfxlim2v  46091  fperdvper  46163  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnprodlem1  46190  stoweidlem27  46271  stoweidlem48  46292  fourierdlem42  46393  fourierdlem63  46413  fourierdlem65  46415  dfsalgen2  46585  subsaliuncl  46602  sge0iunmptlemfi  46657  sge0rpcpnf  46665  iundjiun  46704  psmeasure  46715  ovnsubaddlem2  46815  hoidmvle  46844  ovolval4lem2  46894  smflimlem2  47016  smflimlem3  47017  smflimlem6  47020  smflimmpt  47054  fcoresf1  47315  icceuelpart  47682  gpgedgvtx0  48307  gpgedgvtx1  48308  srhmsubcALTV  48571  catprs  49256  thincciso2  49700  functermclem  49752  functermc  49753  fulltermc  49756