Theorem adantrl 714

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  ad2ant2l  744  ad2ant2rl  747  cases2ALT  1046  consensus  1050  3ad2antr2  1186  3ad2antr3  1187  po2ne  5614  opabssxpd  5733  frpoind  6359  wfiOLD  6368  ordelord  6402  f1un  6867  f1cofveqaeqALT  7279  isocnv  7348  isores2  7351  f1oiso2  7370  offval  7704  ordsucun  7842  xp2nd  8044  2ndconst  8123  sexp2  8168  wfrdmclOLD  8355  smoord  8403  tfrlem9  8423  tfrlem11  8426  oaass  8599  omordi  8604  omwordri  8610  odi  8617  oewordri  8630  nnawordi  8659  nnmordi  8669  coflton  8709  dom2lem  9031  fundmen  9075  sbthlem9  9136  mapen  9186  mapunen  9191  ssenen  9196  domfi  9234  mapfien  9458  inf3lem6  9683  ttrclselem2  9776  frind  9800  r1val1  9836  rankval3b  9876  numacn  10099  infxpabs  10261  infxp  10264  cfsmolem  10320  infpssrlem4  10356  fin23lem27  10378  isf34lem4  10427  hsmexlem2  10477  axdc3lem2  10501  axdc3lem4  10503  iundom2g  10590  gchen1  10675  fpwwe2lem6  10686  fpwwe2lem10  10690  fpwwe2lem11  10691  prlem936  11097  muladd  11703  leord1  11798  eqord1  11799  ltord2  11800  leord2  11801  eqord2  11802  divadddiv  11990  ltmul12a  12131  lemul12b  12132  fimaxre  12220  supadd  12244  supmullem1  12246  cju  12270  zextlt  12698  zmax  12991  xrre  13212  supxr  13356  ixxdisj  13403  iooshf  13467  icodisj  13517  ioojoin  13524  iccshftr  13527  iccshftl  13529  iccdil  13531  icccntr  13533  iccf1o  13537  fzaddel  13599  fzsubel  13601  modadd1  13939  modmul1  13955  seqcaopr  14070  expsub  14141  expmordi  14197  sqlecan  14238  facndiv  14317  hashss  14438  hashfacen  14483  hashfacenOLD  14484  hashf1lem1  14485  hashf1lem1OLD  14486  fi1uzind  14537  brfi1indALT  14540  ccatpfx  14730  swrdccatfn  14753  swrdccatin2  14758  2cshwcshw  14855  resqrex  15276  fprodeq0  15998  lcmdvds  16630  hashdvds  16798  eulerthlem2  16805  pceu  16869  pcqcl  16879  infpnlem1  16933  4sqlem11  16978  ramcl  17052  prmgaplem5  17078  imasvscafn  17573  invfun  17801  initoeu2lem2  18058  catcisolem  18153  funcestrcsetclem8  18192  fullestrcsetc  18196  embedsetcestrclem  18202  funcsetcestrclem8  18207  fullsetcestrc  18211  prfcl  18248  prf1st  18249  prf2nd  18250  1st2ndprf  18251  curfuncf  18284  ipodrsfi  18585  mgmhmpropd  18712  subsubmgm  18724  mhmpropd  18803  subsubm  18827  pwsdiagmhm  18842  frmdgsum  18873  grplcan  19016  grplmulf1o  19029  grpraddf1o  19030  dfgrp3lem  19054  mulgsubcl  19104  subsubg  19165  eqger  19194  qus0subgadd  19215  resghm  19248  conjghm  19265  orbsta  19329  psgnunilem2  19515  odmulg  19576  sylow2a  19639  sylow3lem1  19647  lsmssv  19663  pj1ghm  19723  frgpup1  19795  ghmplusg  19866  subsubrng  20567  subsubrg  20604  srhmsubc  20680  issrngd  20856  lmhmco  21043  lmhmf1o  21046  lmhmima  21047  lmhmpreima  21048  reslmhm  21052  pwsdiaglmhm  21057  pwssplit2  21060  pwssplit3  21061  pj1lmhm  21100  lspdisj  21128  rngqiprngghmlem2  21299  rngqiprngghm  21310  prmirred  21486  cygznlem3  21589  frlmsslsp  21816  frlmlbs  21817  frlmup1  21818  issubassa2  21911  psrbagconf1o  21956  psrbagconf1oOLD  21957  psrgrp  21987  evlslem2  22116  evlslem1  22119  ply1sclf1  22302  mamuass  22416  dmatmul  22513  dmatsubcl  22514  dmatmulcl  22516  dmatcrng  22518  scmatcrng  22537  mdetunilem9  22636  pm2mpghm  22832  fvmptnn04ifb  22867  toponmre  23111  neiptopreu  23151  ordtbas  23210  txcls  23622  txlm  23666  qtoptop2  23717  qtoprest  23735  kqt0lem  23754  ptuncnv  23825  fmfnfmlem4  23975  alexsubALTlem2  24066  tgpmulg  24111  blin  24441  xmeter  24453  xmetresbl  24457  dscmet  24595  nmdvr  24701  metnrmlem3  24891  icccvx  24989  bndth  24998  htpycc  25020  pcohtpylem  25060  pi1blem  25080  lmmbrf  25304  iscfil2  25308  iscau4  25321  minveclem7  25477  elovolm  25518  dyaddisjlem  25638  ismbfd  25682  itg1mulc  25748  dvlip  26040  dvcvx  26067  plypf1  26262  eff1olem  26598  logccv  26713  lawcos  26867  leibpilem1  26991  sqff1o  27233  dvdsppwf1o  27237  dvdsflf1o  27238  fsumdvdsmul  27246  fsumdvdsmulOLD  27248  sgmmul  27253  fsumvma  27265  bposlem6  27341  lgsdchr  27407  rpvmasum2  27564  pntpbnd1  27638  ostthlem1  27679  sltres  27715  nodenselem5  27741  nodenselem6  27742  nodense  27745  addsproplem2  28007  mulsuniflem  28173  mulsunif2lem  28193  precsexlem9  28237  precsexlem10  28238  precsexlem11  28239  om2noseqlt2  28297  om2noseqf1o  28298  tgbtwntriv2  28437  ercgrg  28467  hlpasch  28706  colinearalglem4  28866  axlowdimlem15  28913  axcontlem7  28927  axcontlem8  28928  axcontlem10  28930  usgr1v  29215  pthdivtx  29689  clwwlkn1loopb  29999  grpolcan  30486  nvmf  30601  sspmval  30689  nmosetre  30720  minvecolem7  30839  hiassdi  31047  shscli  31273  fh1  31574  fh2  31575  cm2j  31576  chscllem2  31594  spansncvi  31608  5oalem2  31611  adjsym  31789  nmopsetretALT  31819  nmfnsetre  31833  cnvadj  31848  cnvunop  31874  unoplin  31876  hmoplin  31898  lnopmi  31956  hmops  31976  hmopm  31977  nmcexi  31982  adjlnop  32042  adjmul  32048  adjadd  32049  opsqrlem1  32096  mdsl0  32266  ssmd2  32268  mdexchi  32291  superpos  32310  chrelat2i  32321  atcvatlem  32341  atcvati  32342  chirredlem1  32346  chirredi  32350  atcvat3i  32352  atcvat4i  32353  mdsymlem3  32361  mdsymlem5  32363  cdj3lem2b  32393  ifnebib  32496  isoun  32638  xrge0infss  32692  1arithufdlem3  33452  extdg1id  33583  ddemeas  34107  fsum2dsub  34491  hgt750lemb  34540  bnj1145  34876  subfacp1lem3  35048  subfacp1lem5  35050  cvxpconn  35108  satfv1lem  35228  btwnconn1lem12  35960  colinbtwnle  35980  broutsideof2  35984  lineelsb2  36010  nn0prpwlem  36073  neibastop2lem  36111  tailfb  36128  onsuct0  36192  finxpreclem2  37135  lindsenlbs  37354  poimirlem4  37363  poimirlem26  37385  poimirlem27  37386  poimirlem31  37390  heicant  37394  mblfinlem2  37397  mblfinlem3  37398  ismblfin  37400  ftc1anclem5  37436  ftc1anclem6  37437  ftc1anc  37440  sdclem1  37482  seqpo  37486  sstotbnd  37514  cntotbnd  37535  ismtycnv  37541  ismtyres  37547  heibor  37560  exidreslem  37616  ghomdiv  37631  grpokerinj  37632  rngohomco  37713  rngoisoco  37721  idlsubcl  37762  divrngidl  37767  ispridl2  37777  ispridlc  37809  riotasv3d  38696  omllaw3  38981  omlfh1N  38994  hlrelat2  39140  cvratlem  39158  cvrat  39159  cvrat3  39179  cvrat4  39180  ps-2  39215  elpaddn0  39537  paddss12  39556  pmodlem2  39584  cdleme0cq  39952  cdlemeg49lebilem  40276  cdleme50eq  40278  tendoeq2  40511  tendoex  40712  diameetN  40793  diainN  40794  dvhopN  40853  djajN  40874  dihmeetcl  41082  mapdheq2  41466  3factsumint1  41758  metakunt16  41953  imacrhmcl  42229  psrmnd  42260  evlsvvval  42278  evlselvlem  42301  fsuppind  42305  0prjspn  42343  fphpdo  42536  pell1234qrne0  42572  pell14qrgt0  42578  pell1qrge1  42589  monotoddzzfi  42662  jm2.18  42708  wepwsolem  42765  dnnumch3  42770  dnwech  42771  kelac1  42786  kercvrlsm  42806  onov0suclim  43002  cantnfresb  43052  dssmapnvod  43749  gsumws3  43925  gsumws4  43926  mnuprdlem1  44008  mnuprdlem2  44009  cncmpmax  44693  fiiuncl  44728  choicefi  44868  fvelima2  44930  mullimc  45298  mullimcf  45305  idlimc  45308  limclner  45333  climleltrp  45358  limsupub  45386  climuzlem  45425  climliminflimsup2  45491  xlimbr  45509  xlimxrre  45513  dfxlim2v  45529  fperdvper  45601  ioodvbdlimc1lem2  45614  ioodvbdlimc2lem  45616  dvnprodlem1  45628  stoweidlem27  45709  stoweidlem48  45730  fourierdlem42  45831  fourierdlem63  45851  fourierdlem65  45853  dfsalgen2  46023  subsaliuncl  46040  sge0iunmptlemfi  46095  sge0rpcpnf  46103  iundjiun  46142  psmeasure  46153  ovnsubaddlem2  46253  hoidmvle  46282  ovolval4lem2  46332  smflimlem2  46454  smflimlem3  46455  smflimlem6  46458  smflimmpt  46492  fcoresf1  46745  icceuelpart  47069  srhmsubcALTV  47774  catprs  48404