Theorem adantrl 713

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ad2ant2l  743  ad2ant2rl  746  cases2ALT  1046  consensus  1050  3ad2antr2  1188  3ad2antr3  1189  po2ne  5520  opabssxpd  5635  frpoind  6249  wfiOLD  6258  ordelord  6292  f1un  6745  f1cofveqaeqALT  7141  isocnv  7210  isores2  7213  f1oiso2  7232  offval  7551  ordsucun  7681  xp2nd  7873  2ndconst  7950  wfrdmclOLD  8157  smoord  8205  tfrlem9  8225  tfrlem11  8228  oaass  8401  omordi  8406  omwordri  8412  odi  8419  oewordri  8432  nnawordi  8461  nnmordi  8471  dom2lem  8789  fundmen  8830  sbthlem9  8887  mapen  8937  mapunen  8942  ssenen  8947  domfi  8984  mapfien  9176  inf3lem6  9400  ttrclselem2  9493  frind  9517  r1val1  9553  rankval3b  9593  numacn  9814  infxpabs  9977  infxp  9980  cfsmolem  10035  infpssrlem4  10071  fin23lem27  10093  isf34lem4  10142  hsmexlem2  10192  axdc3lem2  10216  axdc3lem4  10218  iundom2g  10305  gchen1  10390  fpwwe2lem6  10401  fpwwe2lem10  10405  fpwwe2lem11  10406  prlem936  10812  muladd  11416  leord1  11511  eqord1  11512  ltord2  11513  leord2  11514  eqord2  11515  divadddiv  11699  ltmul12a  11840  lemul12b  11841  fimaxre  11928  supadd  11952  supmullem1  11954  cju  11978  zextlt  12403  zmax  12694  xrre  12912  supxr  13056  ixxdisj  13103  iooshf  13167  icodisj  13217  ioojoin  13224  iccshftr  13227  iccshftl  13229  iccdil  13231  icccntr  13233  iccf1o  13237  fzaddel  13299  fzsubel  13301  modadd1  13637  modmul1  13653  seqcaopr  13769  expsub  13840  expmordi  13894  sqlecan  13934  facndiv  14011  hashss  14133  hashfacen  14175  hashfacenOLD  14176  hashf1lem1  14177  hashf1lem1OLD  14178  fi1uzind  14220  brfi1indALT  14223  ccatpfx  14423  swrdccatfn  14446  swrdccatin2  14451  2cshwcshw  14547  resqrex  14971  fprodeq0  15694  lcmdvds  16322  hashdvds  16485  eulerthlem2  16492  pceu  16556  pcqcl  16566  infpnlem1  16620  4sqlem11  16665  ramcl  16739  prmgaplem5  16765  imasvscafn  17257  invfun  17485  initoeu2lem2  17739  catcisolem  17834  funcestrcsetclem8  17873  fullestrcsetc  17877  embedsetcestrclem  17883  funcsetcestrclem8  17888  fullsetcestrc  17892  prfcl  17929  prf1st  17930  prf2nd  17931  1st2ndprf  17932  curfuncf  17965  ipodrsfi  18266  mhmpropd  18445  subsubm  18464  pwsdiagmhm  18478  gsumccatOLD  18488  frmdgsum  18510  grplcan  18646  grplmulf1o  18658  dfgrp3lem  18682  mulgsubcl  18727  subsubg  18787  eqger  18815  resghm  18859  conjghm  18874  orbsta  18928  psgnunilem2  19112  odmulg  19172  sylow2a  19233  sylow3lem1  19241  lsmssv  19257  pj1ghm  19318  frgpup1  19390  ghmplusg  19456  subsubrg  20059  issrngd  20130  lmhmco  20314  lmhmf1o  20317  lmhmima  20318  lmhmpreima  20319  reslmhm  20323  pwsdiaglmhm  20328  pwssplit2  20331  pwssplit3  20332  pj1lmhm  20371  lspdisj  20396  prmirred  20705  cygznlem3  20786  frlmsslsp  21012  frlmlbs  21013  frlmup1  21014  issubassa2  21105  psrbagconf1o  21148  psrbagconf1oOLD  21149  evlslem2  21298  evlslem1  21301  ply1sclf1  21469  mamuass  21558  dmatmul  21655  dmatsubcl  21656  dmatmulcl  21658  dmatcrng  21660  scmatcrng  21679  mdetunilem9  21778  pm2mpghm  21974  fvmptnn04ifb  22009  toponmre  22253  neiptopreu  22293  ordtbas  22352  txcls  22764  txlm  22808  qtoptop2  22859  qtoprest  22877  kqt0lem  22896  ptuncnv  22967  fmfnfmlem4  23117  alexsubALTlem2  23208  tgpmulg  23253  blin  23583  xmeter  23595  xmetresbl  23599  dscmet  23737  nmdvr  23843  metnrmlem3  24033  icccvx  24122  bndth  24130  htpycc  24152  pcohtpylem  24191  pi1blem  24211  lmmbrf  24435  iscfil2  24439  iscau4  24452  minveclem7  24608  elovolm  24648  dyaddisjlem  24768  ismbfd  24812  itg1mulc  24878  dvlip  25166  dvcvx  25193  plypf1  25382  eff1olem  25713  logccv  25827  lawcos  25975  leibpilem1  26099  sqff1o  26340  dvdsppwf1o  26344  dvdsflf1o  26345  fsumdvdsmul  26353  sgmmul  26358  fsumvma  26370  bposlem6  26446  lgsdchr  26512  rpvmasum2  26669  pntpbnd1  26743  ostthlem1  26784  tgbtwntriv2  26857  ercgrg  26887  hlpasch  27126  colinearalglem4  27286  axlowdimlem15  27333  axcontlem7  27347  axcontlem8  27348  axcontlem10  27350  usgr1v  27632  pthdivtx  28106  clwwlkn1loopb  28416  grpolcan  28901  nvmf  29016  sspmval  29104  nmosetre  29135  minvecolem7  29254  hiassdi  29462  shscli  29688  fh1  29989  fh2  29990  cm2j  29991  chscllem2  30009  spansncvi  30023  5oalem2  30026  adjsym  30204  nmopsetretALT  30234  nmfnsetre  30248  cnvadj  30263  cnvunop  30289  unoplin  30291  hmoplin  30313  lnopmi  30371  hmops  30391  hmopm  30392  nmcexi  30397  adjlnop  30457  adjmul  30463  adjadd  30464  opsqrlem1  30511  mdsl0  30681  ssmd2  30683  mdexchi  30706  superpos  30725  chrelat2i  30736  atcvatlem  30756  atcvati  30757  chirredlem1  30761  chirredi  30765  atcvat3i  30767  atcvat4i  30768  mdsymlem3  30776  mdsymlem5  30778  cdj3lem2b  30808  isoun  31043  xrge0infss  31092  extdg1id  31747  ddemeas  32213  fsum2dsub  32596  hgt750lemb  32645  bnj1145  32982  subfacp1lem3  33153  subfacp1lem5  33155  satfv1lem  33333  sexp2  33802  sltres  33874  nodenselem5  33900  nodenselem6  33901  nodense  33904  btwnconn1lem12  34409  colinbtwnle  34429  broutsideof2  34433  lineelsb2  34459  nn0prpwlem  34520  neibastop2lem  34558  tailfb  34575  onsuct0  34639  finxpreclem2  35570  lindsenlbs  35781  poimirlem4  35790  poimirlem26  35812  poimirlem27  35813  poimirlem31  35817  heicant  35821  mblfinlem2  35824  mblfinlem3  35825  ismblfin  35827  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anc  35867  sdclem1  35910  seqpo  35914  sstotbnd  35942  cntotbnd  35963  ismtycnv  35969  ismtyres  35975  heibor  35988  exidreslem  36044  ghomdiv  36059  grpokerinj  36060  rngohomco  36141  rngoisoco  36149  idlsubcl  36190  divrngidl  36195  ispridl2  36205  ispridlc  36237  riotasv3d  36981  omllaw3  37266  omlfh1N  37279  hlrelat2  37424  cvratlem  37442  cvrat  37443  cvrat3  37463  cvrat4  37464  ps-2  37499  elpaddn0  37821  paddss12  37840  pmodlem2  37868  cdleme0cq  38236  cdlemeg49lebilem  38560  cdleme50eq  38562  tendoeq2  38795  tendoex  38996  diameetN  39077  diainN  39078  dvhopN  39137  djajN  39158  dihmeetcl  39366  mapdheq2  39750  3factsumint1  40036  metakunt16  40147  evlsbagval  40282  fsuppind  40286  mhphf  40292  0prjspn  40472  fphpdo  40646  pell1234qrne0  40682  pell14qrgt0  40688  pell1qrge1  40699  monotoddzzfi  40771  jm2.18  40817  wepwsolem  40874  dnnumch3  40879  dnwech  40880  kelac1  40895  kercvrlsm  40915  dssmapnvod  41635  gsumws3  41814  gsumws4  41815  mnuprdlem1  41897  mnuprdlem2  41898  cncmpmax  42582  fiiuncl  42620  choicefi  42747  fvelima2  42813  mullimc  43164  mullimcf  43171  idlimc  43174  limclner  43199  climleltrp  43224  limsupub  43252  climuzlem  43291  climliminflimsup2  43357  xlimbr  43375  xlimxrre  43379  dfxlim2v  43395  fperdvper  43467  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnprodlem1  43494  stoweidlem27  43575  stoweidlem48  43596  fourierdlem42  43697  fourierdlem63  43717  fourierdlem65  43719  dfsalgen2  43887  subsaliuncl  43904  sge0iunmptlemfi  43958  sge0rpcpnf  43966  iundjiun  44005  psmeasure  44016  ovnsubaddlem2  44116  hoidmvle  44145  ovolval4lem2  44195  ovolval5lem3  44199  smflimlem2  44317  smflimlem3  44318  smflimlem6  44321  smflimmpt  44354  fcoresf1  44574  icceuelpart  44899  mgmhmpropd  45350  subsubmgm  45362  srhmsubc  45645  srhmsubcALTV  45663  catprs  46303