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  5577  opabssxpd  5701  frpoind  6331  wfiOLD  6340  ordelord  6374  f1un  6837  fvelima2  6930  f1cofveqaeqALT  7250  isocnv  7322  isores2  7325  f1oiso2  7344  offval  7678  ordsucun  7817  xp2nd  8019  2ndconst  8098  sexp2  8143  wfrdmclOLD  8329  smoord  8377  tfrlem9  8397  tfrlem11  8400  oaass  8571  omordi  8576  omwordri  8582  odi  8589  oewordri  8602  nnawordi  8631  nnmordi  8641  coflton  8681  dom2lem  9004  fundmen  9043  sbthlem9  9103  mapen  9153  mapunen  9158  ssenen  9163  domfi  9201  mapfien  9418  inf3lem6  9645  ttrclselem2  9738  frind  9762  r1val1  9798  rankval3b  9838  numacn  10061  infxpabs  10223  infxp  10226  cfsmolem  10282  infpssrlem4  10318  fin23lem27  10340  isf34lem4  10389  hsmexlem2  10439  axdc3lem2  10463  axdc3lem4  10465  iundom2g  10552  gchen1  10637  fpwwe2lem6  10648  fpwwe2lem10  10652  fpwwe2lem11  10653  prlem936  11059  muladd  11667  leord1  11762  eqord1  11763  ltord2  11764  leord2  11765  eqord2  11766  divadddiv  11954  ltmul12a  12095  lemul12b  12096  fimaxre  12184  supadd  12208  supmullem1  12210  cju  12234  zextlt  12665  zmax  12959  xrre  13183  supxr  13327  ixxdisj  13375  iooshf  13441  icodisj  13491  ioojoin  13498  iccshftr  13501  iccshftl  13503  iccdil  13505  icccntr  13507  iccf1o  13511  fzaddel  13573  fzsubel  13575  modadd1  13923  modmul1  13940  seqcaopr  14055  expsub  14126  expmordi  14183  sqlecan  14225  facndiv  14304  hashss  14425  hashfacen  14470  hashf1lem1  14471  fi1uzind  14523  brfi1indALT  14526  ccatpfx  14717  swrdccatfn  14740  swrdccatin2  14745  2cshwcshw  14842  resqrex  15267  fprodeq0  15989  lcmdvds  16625  hashdvds  16792  eulerthlem2  16799  pceu  16864  pcqcl  16874  infpnlem1  16928  4sqlem11  16973  ramcl  17047  prmgaplem5  17073  imasvscafn  17549  invfun  17775  initoeu2lem2  18026  catcisolem  18121  funcestrcsetclem8  18157  fullestrcsetc  18161  embedsetcestrclem  18167  funcsetcestrclem8  18172  fullsetcestrc  18176  prfcl  18213  prf1st  18214  prf2nd  18215  1st2ndprf  18216  curfuncf  18248  ipodrsfi  18547  mgmhmpropd  18674  subsubmgm  18686  mhmpropd  18768  subsubm  18792  pwsdiagmhm  18807  frmdgsum  18838  grplcan  18981  grplmulf1o  18994  grpraddf1o  18995  dfgrp3lem  19019  mulgsubcl  19069  subsubg  19130  eqger  19159  qus0subgadd  19180  resghm  19213  conjghm  19230  orbsta  19294  psgnunilem2  19474  odmulg  19535  sylow2a  19598  sylow3lem1  19606  lsmssv  19622  pj1ghm  19682  frgpup1  19754  ghmplusg  19825  subsubrng  20521  subsubrg  20556  srhmsubc  20638  issrngd  20813  lmhmco  20999  lmhmf1o  21002  lmhmima  21003  lmhmpreima  21004  reslmhm  21008  pwsdiaglmhm  21013  pwssplit2  21016  pwssplit3  21017  pj1lmhm  21056  lspdisj  21084  rngqiprngghmlem2  21247  rngqiprngghm  21258  prmirred  21433  cygznlem3  21528  frlmsslsp  21754  frlmlbs  21755  frlmup1  21756  issubassa2  21850  psrbagconf1o  21887  psrgrp  21914  evlslem2  22035  evlslem1  22038  ply1sclf1  22224  mamuass  22338  dmatmul  22433  dmatsubcl  22434  dmatmulcl  22436  dmatcrng  22438  scmatcrng  22457  mdetunilem9  22556  pm2mpghm  22752  fvmptnn04ifb  22787  toponmre  23029  neiptopreu  23069  ordtbas  23128  txcls  23540  txlm  23584  qtoptop2  23635  qtoprest  23653  kqt0lem  23672  ptuncnv  23743  fmfnfmlem4  23893  alexsubALTlem2  23984  tgpmulg  24029  blin  24358  xmeter  24370  xmetresbl  24374  dscmet  24509  nmdvr  24607  metnrmlem3  24799  icccvx  24897  bndth  24906  htpycc  24928  pcohtpylem  24968  pi1blem  24988  lmmbrf  25212  iscfil2  25216  iscau4  25229  minveclem7  25385  elovolm  25426  dyaddisjlem  25546  ismbfd  25590  itg1mulc  25655  dvlip  25948  dvcvx  25975  plypf1  26167  eff1olem  26507  logccv  26622  lawcos  26776  leibpilem1  26900  sqff1o  27142  dvdsppwf1o  27146  dvdsflf1o  27147  fsumdvdsmul  27155  fsumdvdsmulOLD  27157  sgmmul  27162  fsumvma  27174  bposlem6  27250  lgsdchr  27316  rpvmasum2  27473  pntpbnd1  27547  ostthlem1  27588  sltres  27624  nodenselem5  27650  nodenselem6  27651  nodense  27654  addsproplem2  27920  mulsuniflem  28092  mulsunif2lem  28112  precsexlem9  28156  precsexlem10  28157  precsexlem11  28158  om2noseqlt2  28223  om2noseqf1o  28224  tgbtwntriv2  28412  ercgrg  28442  hlpasch  28681  colinearalglem4  28834  axlowdimlem15  28881  axcontlem7  28895  axcontlem8  28896  axcontlem10  28898  usgr1v  29181  pthdivtx  29655  clwwlkn1loopb  29970  grpolcan  30457  nvmf  30572  sspmval  30660  nmosetre  30691  minvecolem7  30810  hiassdi  31018  shscli  31244  fh1  31545  fh2  31546  cm2j  31547  chscllem2  31565  spansncvi  31579  5oalem2  31582  adjsym  31760  nmopsetretALT  31790  nmfnsetre  31804  cnvadj  31819  cnvunop  31845  unoplin  31847  hmoplin  31869  lnopmi  31927  hmops  31947  hmopm  31948  nmcexi  31953  adjlnop  32013  adjmul  32019  adjadd  32020  opsqrlem1  32067  mdsl0  32237  ssmd2  32239  mdexchi  32262  superpos  32281  chrelat2i  32292  atcvatlem  32312  atcvati  32313  chirredlem1  32317  chirredi  32321  atcvat3i  32323  atcvat4i  32324  mdsymlem3  32332  mdsymlem5  32334  cdj3lem2b  32364  ifnebib  32476  isoun  32625  xrge0infss  32683  1arithufdlem3  33507  extdg1id  33653  ddemeas  34213  fsum2dsub  34585  hgt750lemb  34634  bnj1145  34970  subfacp1lem3  35150  subfacp1lem5  35152  cvxpconn  35210  satfv1lem  35330  btwnconn1lem12  36062  colinbtwnle  36082  broutsideof2  36086  lineelsb2  36112  nn0prpwlem  36286  neibastop2lem  36324  tailfb  36341  onsuct0  36405  finxpreclem2  37354  lindsenlbs  37585  poimirlem4  37594  poimirlem26  37616  poimirlem27  37617  poimirlem31  37621  heicant  37625  mblfinlem2  37628  mblfinlem3  37629  ismblfin  37631  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anc  37671  sdclem1  37713  seqpo  37717  sstotbnd  37745  cntotbnd  37766  ismtycnv  37772  ismtyres  37778  heibor  37791  exidreslem  37847  ghomdiv  37862  grpokerinj  37863  rngohomco  37944  rngoisoco  37952  idlsubcl  37993  divrngidl  37998  ispridl2  38008  ispridlc  38040  riotasv3d  38924  omllaw3  39209  omlfh1N  39222  hlrelat2  39368  cvratlem  39386  cvrat  39387  cvrat3  39407  cvrat4  39408  ps-2  39443  elpaddn0  39765  paddss12  39784  pmodlem2  39812  cdleme0cq  40180  cdlemeg49lebilem  40504  cdleme50eq  40506  tendoeq2  40739  tendoex  40940  diameetN  41021  diainN  41022  dvhopN  41081  djajN  41102  dihmeetcl  41310  mapdheq2  41694  3factsumint1  41980  metakunt16  42179  imacrhmcl  42484  psrmnd  42515  evlsvvval  42533  evlselvlem  42556  fsuppind  42560  0prjspn  42598  fphpdo  42787  pell1234qrne0  42823  pell14qrgt0  42829  pell1qrge1  42840  monotoddzzfi  42913  jm2.18  42959  wepwsolem  43013  dnnumch3  43018  dnwech  43019  kelac1  43034  kercvrlsm  43054  onov0suclim  43245  cantnfresb  43295  dssmapnvod  43991  gsumws3  44167  gsumws4  44168  mnuprdlem1  44244  mnuprdlem2  44245  traxext  44950  modelac8prim  44965  cncmpmax  45004  fiiuncl  45037  choicefi  45172  mullimc  45593  mullimcf  45600  idlimc  45603  limclner  45628  climleltrp  45653  limsupub  45681  climuzlem  45720  climliminflimsup2  45786  xlimbr  45804  xlimxrre  45808  dfxlim2v  45824  fperdvper  45896  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnprodlem1  45923  stoweidlem27  46004  stoweidlem48  46025  fourierdlem42  46126  fourierdlem63  46146  fourierdlem65  46148  dfsalgen2  46318  subsaliuncl  46335  sge0iunmptlemfi  46390  sge0rpcpnf  46398  iundjiun  46437  psmeasure  46448  ovnsubaddlem2  46548  hoidmvle  46577  ovolval4lem2  46627  smflimlem2  46749  smflimlem3  46750  smflimlem6  46753  smflimmpt  46787  fcoresf1  47046  icceuelpart  47398  gpgedgvtx0  48013  gpgedgvtx1  48014  srhmsubcALTV  48248  catprs  48934  thincciso2  49289  functermclem  49340  functermc  49341  fulltermc  49344