Theorem adantrl 717

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 594	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  747  ad2ant2rl  750  cases2ALT  1049  consensus  1053  3ad2antr2  1191  3ad2antr3  1192  po2ne  5555  opabssxpd  5678  frpoind  6306  ordelord  6345  f1un  6800  fvelima2  6892  f1cofveqaeqALT  7213  isocnv  7285  isores2  7288  f1oiso2  7307  offval  7640  ordsucun  7776  xp2nd  7975  2ndconst  8051  sexp2  8096  smoord  8305  tfrlem9  8324  tfrlem11  8327  oaass  8496  omordi  8501  omwordri  8507  odi  8514  oewordri  8528  nnawordi  8557  nnmordi  8567  coflton  8607  dom2lem  8939  fundmen  8978  sbthlem9  9033  mapen  9079  mapunen  9084  ssenen  9089  domfi  9123  mapfien  9321  inf3lem6  9554  ttrclselem2  9647  frind  9674  r1val1  9710  rankval3b  9750  numacn  9971  infxpabs  10133  infxp  10136  cfsmolem  10192  infpssrlem4  10228  fin23lem27  10250  isf34lem4  10299  hsmexlem2  10349  axdc3lem2  10373  axdc3lem4  10375  iundom2g  10462  gchen1  10548  fpwwe2lem6  10559  fpwwe2lem10  10563  fpwwe2lem11  10564  prlem936  10970  muladd  11582  leord1  11677  eqord1  11678  ltord2  11679  leord2  11680  eqord2  11681  divadddiv  11870  ltmul12a  12011  lemul12b  12012  fimaxre  12100  supadd  12124  supmullem1  12126  cju  12155  zextlt  12603  zmax  12895  xrre  13121  supxr  13265  ixxdisj  13313  iooshf  13379  icodisj  13429  ioojoin  13436  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  iccf1o  13449  fzaddel  13512  fzsubel  13514  modadd1  13867  modmul1  13886  seqcaopr  14001  expsub  14072  expmordi  14129  sqlecan  14171  facndiv  14250  hashss  14371  hashfacen  14416  hashf1lem1  14417  fi1uzind  14469  brfi1indALT  14472  ccatpfx  14663  swrdccatfn  14686  swrdccatin2  14691  2cshwcshw  14787  resqrex  15212  fprodeq0  15940  lcmdvds  16577  hashdvds  16745  eulerthlem2  16752  pceu  16817  pcqcl  16827  infpnlem1  16881  4sqlem11  16926  ramcl  17000  prmgaplem5  17026  imasvscafn  17501  invfun  17731  initoeu2lem2  17982  catcisolem  18077  funcestrcsetclem8  18113  fullestrcsetc  18117  embedsetcestrclem  18123  funcsetcestrclem8  18128  fullsetcestrc  18132  prfcl  18169  prf1st  18170  prf2nd  18171  1st2ndprf  18172  curfuncf  18204  ipodrsfi  18505  mgmhmpropd  18666  subsubmgm  18678  mhmpropd  18760  subsubm  18784  pwsdiagmhm  18799  frmdgsum  18830  grplcan  18976  grplmulf1o  18989  grpraddf1o  18990  dfgrp3lem  19014  mulgsubcl  19064  subsubg  19125  eqger  19153  qus0subgadd  19174  resghm  19207  conjghm  19224  orbsta  19288  psgnunilem2  19470  odmulg  19531  sylow2a  19594  sylow3lem1  19602  lsmssv  19618  pj1ghm  19678  frgpup1  19750  ghmplusg  19821  subsubrng  20540  subsubrg  20575  srhmsubc  20657  issrngd  20832  lmhmco  21038  lmhmf1o  21041  lmhmima  21042  lmhmpreima  21043  reslmhm  21047  pwsdiaglmhm  21052  pwssplit2  21055  pwssplit3  21056  pj1lmhm  21095  lspdisj  21123  rngqiprngghmlem2  21286  rngqiprngghm  21297  prmirred  21454  cygznlem3  21549  frlmsslsp  21776  frlmlbs  21777  frlmup1  21778  issubassa2  21872  psrbagconf1o  21909  psrgrp  21935  evlslem2  22057  evlslem1  22060  evlsvvval  22071  ply1sclf1  22254  mamuass  22367  dmatmul  22462  dmatsubcl  22463  dmatmulcl  22465  dmatcrng  22467  scmatcrng  22486  mdetunilem9  22585  pm2mpghm  22781  fvmptnn04ifb  22816  toponmre  23058  neiptopreu  23098  ordtbas  23157  txcls  23569  txlm  23613  qtoptop2  23664  qtoprest  23682  kqt0lem  23701  ptuncnv  23772  fmfnfmlem4  23922  alexsubALTlem2  24013  tgpmulg  24058  blin  24386  xmeter  24398  xmetresbl  24402  dscmet  24537  nmdvr  24635  metnrmlem3  24827  icccvx  24917  bndth  24925  htpycc  24947  pcohtpylem  24986  pi1blem  25006  lmmbrf  25229  iscfil2  25233  iscau4  25246  minveclem7  25402  elovolm  25442  dyaddisjlem  25562  ismbfd  25606  itg1mulc  25671  dvlip  25960  dvcvx  25987  plypf1  26177  eff1olem  26512  logccv  26627  lawcos  26780  leibpilem1  26904  sqff1o  27145  dvdsppwf1o  27149  dvdsflf1o  27150  fsumdvdsmul  27158  sgmmul  27164  fsumvma  27176  bposlem6  27252  lgsdchr  27318  rpvmasum2  27475  pntpbnd1  27549  ostthlem1  27590  ltsres  27626  nodenselem5  27652  nodenselem6  27653  nodense  27656  addsproplem2  27962  mulsuniflem  28141  mulsunif2lem  28161  precsexlem9  28207  precsexlem10  28208  precsexlem11  28209  om2noseqlt2  28292  om2noseqf1o  28293  z12sge0  28475  elreno2  28487  tgbtwntriv2  28555  ercgrg  28585  hlpasch  28824  colinearalglem4  28978  axlowdimlem15  29025  axcontlem7  29039  axcontlem8  29040  axcontlem10  29042  usgr1v  29325  pthdivtx  29795  clwwlkn1loopb  30113  grpolcan  30601  nvmf  30716  sspmval  30804  nmosetre  30835  minvecolem7  30954  hiassdi  31162  shscli  31388  fh1  31689  fh2  31690  cm2j  31691  chscllem2  31709  spansncvi  31723  5oalem2  31726  adjsym  31904  nmopsetretALT  31934  nmfnsetre  31948  cnvadj  31963  cnvunop  31989  unoplin  31991  hmoplin  32013  lnopmi  32071  hmops  32091  hmopm  32092  nmcexi  32097  adjlnop  32157  adjmul  32163  adjadd  32164  opsqrlem1  32211  mdsl0  32381  ssmd2  32383  mdexchi  32406  superpos  32425  chrelat2i  32436  atcvatlem  32456  atcvati  32457  chirredlem1  32461  chirredi  32465  atcvat3i  32467  atcvat4i  32468  mdsymlem3  32476  mdsymlem5  32478  cdj3lem2b  32508  ifnebib  32619  isoun  32775  xrge0infss  32833  1arithufdlem3  33606  extdg1id  33810  ddemeas  34380  fsum2dsub  34751  hgt750lemb  34800  bnj1145  35135  subfacp1lem3  35364  subfacp1lem5  35366  cvxpconn  35424  satfv1lem  35544  btwnconn1lem12  36280  colinbtwnle  36300  broutsideof2  36304  lineelsb2  36330  nn0prpwlem  36504  neibastop2lem  36542  tailfb  36559  onsuct0  36623  finxpreclem2  37706  lindsenlbs  37936  poimirlem4  37945  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  heicant  37976  mblfinlem2  37979  mblfinlem3  37980  ismblfin  37982  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anc  38022  sdclem1  38064  seqpo  38068  sstotbnd  38096  cntotbnd  38117  ismtycnv  38123  ismtyres  38129  heibor  38142  exidreslem  38198  ghomdiv  38213  grpokerinj  38214  rngohomco  38295  rngoisoco  38303  idlsubcl  38344  divrngidl  38349  ispridl2  38359  ispridlc  38391  riotasv3d  39406  omllaw3  39691  omlfh1N  39704  hlrelat2  39849  cvratlem  39867  cvrat  39868  cvrat3  39888  cvrat4  39889  ps-2  39924  elpaddn0  40246  paddss12  40265  pmodlem2  40293  cdleme0cq  40661  cdlemeg49lebilem  40985  cdleme50eq  40987  tendoeq2  41220  tendoex  41421  diameetN  41502  diainN  41503  dvhopN  41562  djajN  41583  dihmeetcl  41791  mapdheq2  42175  3factsumint1  42460  imacrhmcl  42959  psrmnd  42988  evlselvlem  43019  fsuppind  43023  0prjspn  43061  fphpdo  43245  pell1234qrne0  43281  pell14qrgt0  43287  pell1qrge1  43298  monotoddzzfi  43370  jm2.18  43416  wepwsolem  43470  dnnumch3  43475  dnwech  43476  kelac1  43491  kercvrlsm  43511  onov0suclim  43702  cantnfresb  43752  dssmapnvod  44447  gsumws3  44623  gsumws4  44624  mnuprdlem1  44699  mnuprdlem2  44700  traxext  45404  modelac8prim  45419  cncmpmax  45463  fiiuncl  45496  choicefi  45629  mullimc  46046  mullimcf  46053  idlimc  46056  limclner  46079  climleltrp  46104  limsupub  46132  climuzlem  46171  climliminflimsup2  46237  xlimbr  46255  xlimxrre  46259  dfxlim2v  46275  fperdvper  46347  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnprodlem1  46374  stoweidlem27  46455  stoweidlem48  46476  fourierdlem42  46577  fourierdlem63  46597  fourierdlem65  46599  dfsalgen2  46769  subsaliuncl  46786  sge0iunmptlemfi  46841  sge0rpcpnf  46849  iundjiun  46888  psmeasure  46899  ovnsubaddlem2  46999  hoidmvle  47028  ovolval4lem2  47078  smflimlem2  47200  smflimlem3  47201  smflimlem6  47204  smflimmpt  47238  fcoresf1  47517  icceuelpart  47896  gpgedgvtx0  48537  gpgedgvtx1  48538  srhmsubcALTV  48801  catprs  49486  thincciso2  49930  functermclem  49982  functermc  49983  fulltermc  49986