Theorem adantrl 748

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ad2ant2l  778  ad2ant2rl  781  consensus  990  cases2  1005  3ad2antr2  1220  3ad2antr3  1221  wfi  5630  ordelord  5662  foco  6038  isocnv  6480  isores2  6483  f1oiso2  6502  offval  6802  ordsucun  6917  opabex2  6997  xp2nd  7090  1stconst  7152  2ndconst  7153  wfrdmcl  7310  smoord  7349  tfrlem9  7368  tfrlem11  7371  oaass  7528  omordi  7533  omwordri  7539  odi  7546  oewordri  7559  nnawordi  7588  nnmordi  7598  dom2lem  7881  fundmen  7916  sbthlem9  7963  mapen  8009  mapunen  8014  ssenen  8019  domfi  8066  mapfien  8196  inf3lem6  8413  r1val1  8532  rankval3b  8572  numacn  8755  infxpabs  8917  infxp  8920  cfsmolem  8975  infpssrlem4  9011  fin23lem27  9033  isf34lem4  9082  hsmexlem2  9132  axdc3lem2  9156  axdc3lem4  9158  iundom2g  9241  gchen1  9326  fpwwe2lem7  9337  fpwwe2lem11  9341  fpwwe2lem12  9342  prlem936  9748  muladd  10341  leord1  10434  eqord1  10435  ltord2  10436  leord2  10437  eqord2  10438  divadddiv  10619  ltmul12a  10758  lemul12b  10759  supadd  10868  supmullem1  10870  cju  10893  zextlt  11327  zmax  11661  xrre  11874  supxr  12015  ixxdisj  12061  iooshf  12123  icodisj  12168  ioojoin  12174  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  iccf1o  12187  fzaddel  12246  fzsubel  12248  modadd1  12569  modmul1  12585  seqcaopr  12700  expsub  12770  sqlecan  12833  facndiv  12937  hashss  13058  hashfacen  13095  hashf1lem1  13096  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  swrdccatin12lem2b  13337  2cshwcshw  13422  resqrex  13839  fprodeq0  14544  lcmdvds  15159  hashdvds  15318  eulerthlem2  15325  pceu  15389  pcqcl  15399  infpnlem1  15452  4sqlem11  15497  ramcl  15571  prmgaplem5  15597  imasvscafn  16020  invfun  16247  initoeu2lem2  16488  catcisolem  16579  funcestrcsetclem8  16610  fullestrcsetc  16614  embedsetcestrclem  16620  funcsetcestrclem8  16625  fullsetcestrc  16629  prfcl  16666  prf1st  16667  prf2nd  16668  1st2ndprf  16669  curfuncf  16701  ipodrsfi  16986  mhmpropd  17164  subsubm  17180  pwsdiagmhm  17192  gsumccat  17201  frmdgsum  17222  grplcan  17300  grplmulf1o  17312  dfgrp3lem  17336  mulgsubcl  17378  subsubg  17440  eqger  17467  resghm  17499  conjghm  17514  orbsta  17569  psgnunilem2  17738  odmulg  17796  sylow2a  17857  sylow3lem1  17865  lsmssv  17881  pj1ghm  17939  frgpup1  18011  ghmplusg  18072  subsubrg  18629  issrngd  18684  lmhmco  18864  lmhmf1o  18867  lmhmima  18868  lmhmpreima  18869  reslmhm  18873  pwsdiaglmhm  18878  pwssplit2  18881  pwssplit3  18882  pj1lmhm  18921  lspdisj  18946  issubassa2  19166  psrbagconf1o  19195  evlslem2  19333  evlslem1  19336  ply1sclf1  19480  prmirred  19662  cygznlem3  19737  frlmsslsp  19954  frlmlbs  19955  frlmup1  19956  mamuass  20027  dmatmul  20122  dmatsubcl  20123  dmatmulcl  20125  dmatcrng  20127  scmatcrng  20146  mdetunilem9  20245  pm2mpghm  20440  fvmptnn04ifb  20475  toponmre  20707  neiptopreu  20747  ordtbas  20806  txcls  21217  txlm  21261  qtoptop2  21312  qtoprest  21330  kqt0lem  21349  ptuncnv  21420  fmfnfmlem4  21571  alexsubALTlem2  21662  tgpmulg  21707  blin  22036  xmeter  22048  xmetresbl  22052  dscmet  22187  nmdvr  22284  metnrmlem3  22472  icccvx  22557  bndth  22565  htpycc  22587  pcohtpylem  22627  pi1blem  22647  lmmbrf  22868  iscfil2  22872  iscau4  22885  minveclem7  23014  elovolm  23050  dyaddisjlem  23169  ismbfd  23213  itg1mulc  23277  dvlip  23560  dvcvx  23587  plypf1  23772  eff1olem  24098  logccv  24209  lawcos  24346  sqff1o  24708  dvdsppwf1o  24712  dvdsflf1o  24713  fsumdvdsmul  24721  sgmmul  24726  fsumvma  24738  bposlem6  24814  lgsdchr  24880  rpvmasum2  25001  pntpbnd1  25075  ostthlem1  25116  tgbtwntriv2  25182  ercgrg  25212  hlpasch  25448  colhp  25462  colinearalglem4  25589  axlowdimlem15  25636  axcontlem7  25650  axcontlem8  25651  axcontlem10  25653  spthonepeq  26117  usgra2adedgspth  26141  usgra2adedgwlk  26142  usgra2adedgwlkon  26143  numclwlk1lem2f1  26621  grpolcan  26768  nvmf  26884  sspmval  26972  nmosetre  27003  sspph  27094  minvecolem7  27123  hiassdi  27332  shscli  27560  fh1  27861  fh2  27862  cm2j  27863  chscllem2  27881  spansncvi  27895  5oalem2  27898  adjsym  28076  nmopsetretALT  28106  nmfnsetre  28120  cnvadj  28135  cnvunop  28161  unoplin  28163  hmoplin  28185  lnopmi  28243  hmops  28263  hmopm  28264  nmcexi  28269  adjlnop  28329  adjmul  28335  adjadd  28336  opsqrlem1  28383  mdsl0  28553  ssmd2  28555  mdexchi  28578  superpos  28597  chrelat2i  28608  atcvatlem  28628  atcvati  28629  chirredlem1  28633  chirredi  28637  atcvat3i  28639  atcvat4i  28640  mdsymlem3  28648  mdsymlem5  28650  cdj3lem2b  28680  isoun  28862  xrge0infss  28915  ddemeas  29626  bnj1145  30315  subfacp1lem3  30418  subfacp1lem5  30420  frind  30984  sltres  31061  nodenselem6  31085  nodenselem7  31086  nodense  31088  nofulllem5  31105  btwnconn1lem12  31375  colinbtwnle  31395  broutsideof2  31399  lineelsb2  31425  nn0prpwlem  31487  neibastop2lem  31525  tailfb  31542  onsuct0  31610  finxpreclem2  32403  lindsenlbs  32574  poimirlem4  32583  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  ismblfin  32620  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anc  32663  sdclem1  32709  seqpo  32713  sstotbnd  32744  cntotbnd  32765  ismtycnv  32771  ismtyres  32777  heibor  32790  exidreslem  32846  ghomdiv  32861  grpokerinj  32862  rngohomco  32943  rngoisoco  32951  idlsubcl  32992  divrngidl  32997  ispridl2  33007  ispridlc  33039  riotasv3d  33264  omllaw3  33550  omlfh1N  33563  hlrelat2  33707  cvratlem  33725  cvrat  33726  cvrat3  33746  cvrat4  33747  ps-2  33782  elpaddn0  34104  paddss12  34123  pmodlem2  34151  cdleme0cq  34520  cdlemeg49lebilem  34845  cdleme50eq  34847  tendoeq2  35080  tendoex  35281  diameetN  35363  diainN  35364  dvhopN  35423  djajN  35444  dihmeetcl  35652  mapdheq2  36036  fphpdo  36399  pell1234qrne0  36435  pell14qrgt0  36441  pell1qrge1  36452  monotoddzzfi  36525  expmordi  36530  jm2.18  36573  wepwsolem  36630  dnnumch3  36635  dnwech  36636  kelac1  36651  kercvrlsm  36671  dssmapnvod  37334  gsumws3  37521  gsumws4  37522  cncmpmax  38214  fiiuncl  38259  choicefi  38387  mullimc  38683  mullimcf  38690  idlimc  38693  limclner  38718  climleltrp  38743  fperdvper  38808  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnprodlem1  38836  stoweidlem27  38920  stoweidlem48  38941  fourierdlem42  39042  fourierdlem63  39062  fourierdlem65  39064  dfsalgen2  39235  subsaliuncl  39252  sge0iunmptlemfi  39306  sge0rpcpnf  39314  iundjiun  39353  psmeasure  39364  ovnsubaddlem2  39461  hoidmvle  39490  ovolval4lem2  39540  ovolval5lem3  39544  smflimlem2  39658  smflimlem3  39659  smflimlem6  39662  icceuelpart  39974  f1cofveqaeqALT  40324  usgr1v  40482  pthdivtx  40935  mgmhmpropd  41575  subsubmgm  41587  srhmsubc  41868  srhmsubcALTV  41887