Theorem adantrl 712

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 592	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 206  df-an 396

This theorem is referenced by:  ad2ant2l  742  ad2ant2rl  745  cases2ALT  1045  consensus  1049  3ad2antr2  1187  3ad2antr3  1188  po2ne  5510  opabssxpd  5625  frpoind  6230  wfiOLD  6239  ordelord  6273  f1cofveqaeqALT  7113  isocnv  7181  isores2  7184  f1oiso2  7203  offval  7520  ordsucun  7647  xp2nd  7837  2ndconst  7912  wfrdmclOLD  8119  smoord  8167  tfrlem9  8187  tfrlem11  8190  oaass  8354  omordi  8359  omwordri  8365  odi  8372  oewordri  8385  nnawordi  8414  nnmordi  8424  dom2lem  8735  fundmen  8775  sbthlem9  8831  mapen  8877  mapunen  8882  ssenen  8887  domfi  8935  mapfien  9097  inf3lem6  9321  frind  9439  r1val1  9475  rankval3b  9515  numacn  9736  infxpabs  9899  infxp  9902  cfsmolem  9957  infpssrlem4  9993  fin23lem27  10015  isf34lem4  10064  hsmexlem2  10114  axdc3lem2  10138  axdc3lem4  10140  iundom2g  10227  gchen1  10312  fpwwe2lem6  10323  fpwwe2lem10  10327  fpwwe2lem11  10328  prlem936  10734  muladd  11337  leord1  11432  eqord1  11433  ltord2  11434  leord2  11435  eqord2  11436  divadddiv  11620  ltmul12a  11761  lemul12b  11762  fimaxre  11849  supadd  11873  supmullem1  11875  cju  11899  zextlt  12324  zmax  12614  xrre  12832  supxr  12976  ixxdisj  13023  iooshf  13087  icodisj  13137  ioojoin  13144  iccshftr  13147  iccshftl  13149  iccdil  13151  icccntr  13153  iccf1o  13157  fzaddel  13219  fzsubel  13221  modadd1  13556  modmul1  13572  seqcaopr  13688  expsub  13759  expmordi  13813  sqlecan  13853  facndiv  13930  hashss  14052  hashfacen  14094  hashfacenOLD  14095  hashf1lem1  14096  hashf1lem1OLD  14097  fi1uzind  14139  brfi1indALT  14142  ccatpfx  14342  swrdccatfn  14365  swrdccatin2  14370  2cshwcshw  14466  resqrex  14890  fprodeq0  15613  lcmdvds  16241  hashdvds  16404  eulerthlem2  16411  pceu  16475  pcqcl  16485  infpnlem1  16539  4sqlem11  16584  ramcl  16658  prmgaplem5  16684  imasvscafn  17165  invfun  17393  initoeu2lem2  17646  catcisolem  17741  funcestrcsetclem8  17780  fullestrcsetc  17784  embedsetcestrclem  17790  funcsetcestrclem8  17795  fullsetcestrc  17799  prfcl  17836  prf1st  17837  prf2nd  17838  1st2ndprf  17839  curfuncf  17872  ipodrsfi  18172  mhmpropd  18351  subsubm  18370  pwsdiagmhm  18384  gsumccatOLD  18394  frmdgsum  18416  grplcan  18552  grplmulf1o  18564  dfgrp3lem  18588  mulgsubcl  18633  subsubg  18693  eqger  18721  resghm  18765  conjghm  18780  orbsta  18834  psgnunilem2  19018  odmulg  19078  sylow2a  19139  sylow3lem1  19147  lsmssv  19163  pj1ghm  19224  frgpup1  19296  ghmplusg  19362  subsubrg  19965  issrngd  20036  lmhmco  20220  lmhmf1o  20223  lmhmima  20224  lmhmpreima  20225  reslmhm  20229  pwsdiaglmhm  20234  pwssplit2  20237  pwssplit3  20238  pj1lmhm  20277  lspdisj  20302  prmirred  20608  cygznlem3  20689  frlmsslsp  20913  frlmlbs  20914  frlmup1  20915  issubassa2  21006  psrbagconf1o  21049  psrbagconf1oOLD  21050  evlslem2  21199  evlslem1  21202  ply1sclf1  21370  mamuass  21459  dmatmul  21554  dmatsubcl  21555  dmatmulcl  21557  dmatcrng  21559  scmatcrng  21578  mdetunilem9  21677  pm2mpghm  21873  fvmptnn04ifb  21908  toponmre  22152  neiptopreu  22192  ordtbas  22251  txcls  22663  txlm  22707  qtoptop2  22758  qtoprest  22776  kqt0lem  22795  ptuncnv  22866  fmfnfmlem4  23016  alexsubALTlem2  23107  tgpmulg  23152  blin  23482  xmeter  23494  xmetresbl  23498  dscmet  23634  nmdvr  23740  metnrmlem3  23930  icccvx  24019  bndth  24027  htpycc  24049  pcohtpylem  24088  pi1blem  24108  lmmbrf  24331  iscfil2  24335  iscau4  24348  minveclem7  24504  elovolm  24544  dyaddisjlem  24664  ismbfd  24708  itg1mulc  24774  dvlip  25062  dvcvx  25089  plypf1  25278  eff1olem  25609  logccv  25723  lawcos  25871  leibpilem1  25995  sqff1o  26236  dvdsppwf1o  26240  dvdsflf1o  26241  fsumdvdsmul  26249  sgmmul  26254  fsumvma  26266  bposlem6  26342  lgsdchr  26408  rpvmasum2  26565  pntpbnd1  26639  ostthlem1  26680  tgbtwntriv2  26752  ercgrg  26782  hlpasch  27021  colinearalglem4  27180  axlowdimlem15  27227  axcontlem7  27241  axcontlem8  27242  axcontlem10  27244  usgr1v  27526  pthdivtx  27998  clwwlkn1loopb  28308  grpolcan  28793  nvmf  28908  sspmval  28996  nmosetre  29027  minvecolem7  29146  hiassdi  29354  shscli  29580  fh1  29881  fh2  29882  cm2j  29883  chscllem2  29901  spansncvi  29915  5oalem2  29918  adjsym  30096  nmopsetretALT  30126  nmfnsetre  30140  cnvadj  30155  cnvunop  30181  unoplin  30183  hmoplin  30205  lnopmi  30263  hmops  30283  hmopm  30284  nmcexi  30289  adjlnop  30349  adjmul  30355  adjadd  30356  opsqrlem1  30403  mdsl0  30573  ssmd2  30575  mdexchi  30598  superpos  30617  chrelat2i  30628  atcvatlem  30648  atcvati  30649  chirredlem1  30653  chirredi  30657  atcvat3i  30659  atcvat4i  30660  mdsymlem3  30668  mdsymlem5  30670  cdj3lem2b  30700  isoun  30936  xrge0infss  30985  extdg1id  31640  ddemeas  32104  fsum2dsub  32487  hgt750lemb  32536  bnj1145  32873  subfacp1lem3  33044  subfacp1lem5  33046  satfv1lem  33224  ttrclselem2  33712  sexp2  33720  sltres  33792  nodenselem5  33818  nodenselem6  33819  nodense  33822  btwnconn1lem12  34327  colinbtwnle  34347  broutsideof2  34351  lineelsb2  34377  nn0prpwlem  34438  neibastop2lem  34476  tailfb  34493  onsuct0  34557  finxpreclem2  35488  lindsenlbs  35699  poimirlem4  35708  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  heicant  35739  mblfinlem2  35742  mblfinlem3  35743  ismblfin  35745  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anc  35785  sdclem1  35828  seqpo  35832  sstotbnd  35860  cntotbnd  35881  ismtycnv  35887  ismtyres  35893  heibor  35906  exidreslem  35962  ghomdiv  35977  grpokerinj  35978  rngohomco  36059  rngoisoco  36067  idlsubcl  36108  divrngidl  36113  ispridl2  36123  ispridlc  36155  riotasv3d  36901  omllaw3  37186  omlfh1N  37199  hlrelat2  37344  cvratlem  37362  cvrat  37363  cvrat3  37383  cvrat4  37384  ps-2  37419  elpaddn0  37741  paddss12  37760  pmodlem2  37788  cdleme0cq  38156  cdlemeg49lebilem  38480  cdleme50eq  38482  tendoeq2  38715  tendoex  38916  diameetN  38997  diainN  38998  dvhopN  39057  djajN  39078  dihmeetcl  39286  mapdheq2  39670  3factsumint1  39957  metakunt16  40068  evlsbagval  40198  fsuppind  40202  mhphf  40208  0prjspn  40386  fphpdo  40555  pell1234qrne0  40591  pell14qrgt0  40597  pell1qrge1  40608  monotoddzzfi  40680  jm2.18  40726  wepwsolem  40783  dnnumch3  40788  dnwech  40789  kelac1  40804  kercvrlsm  40824  dssmapnvod  41517  gsumws3  41696  gsumws4  41697  mnuprdlem1  41779  mnuprdlem2  41780  cncmpmax  42464  fiiuncl  42502  choicefi  42629  fvelima2  42695  mullimc  43047  mullimcf  43054  idlimc  43057  limclner  43082  climleltrp  43107  limsupub  43135  climuzlem  43174  climliminflimsup2  43240  xlimbr  43258  xlimxrre  43262  dfxlim2v  43278  fperdvper  43350  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnprodlem1  43377  stoweidlem27  43458  stoweidlem48  43479  fourierdlem42  43580  fourierdlem63  43600  fourierdlem65  43602  dfsalgen2  43770  subsaliuncl  43787  sge0iunmptlemfi  43841  sge0rpcpnf  43849  iundjiun  43888  psmeasure  43899  ovnsubaddlem2  43999  hoidmvle  44028  ovolval4lem2  44078  ovolval5lem3  44082  smflimlem2  44194  smflimlem3  44195  smflimlem6  44198  smflimmpt  44230  fcoresf1  44450  icceuelpart  44776  mgmhmpropd  45227  subsubmgm  45239  srhmsubc  45522  srhmsubcALTV  45540  catprs  46180