Theorem adantrl 715

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  ad2ant2l  745  ad2ant2rl  748  cases2ALT  1048  consensus  1052  3ad2antr2  1190  3ad2antr3  1191  po2ne  5605  opabssxpd  5724  frpoind  6344  wfiOLD  6353  ordelord  6387  f1un  6854  f1cofveqaeqALT  7258  isocnv  7327  isores2  7330  f1oiso2  7349  offval  7679  ordsucun  7813  xp2nd  8008  2ndconst  8087  sexp2  8132  wfrdmclOLD  8317  smoord  8365  tfrlem9  8385  tfrlem11  8388  oaass  8561  omordi  8566  omwordri  8572  odi  8579  oewordri  8592  nnawordi  8621  nnmordi  8631  coflton  8670  dom2lem  8988  fundmen  9031  sbthlem9  9091  mapen  9141  mapunen  9146  ssenen  9151  domfi  9192  mapfien  9403  inf3lem6  9628  ttrclselem2  9721  frind  9745  r1val1  9781  rankval3b  9821  numacn  10044  infxpabs  10207  infxp  10210  cfsmolem  10265  infpssrlem4  10301  fin23lem27  10323  isf34lem4  10372  hsmexlem2  10422  axdc3lem2  10446  axdc3lem4  10448  iundom2g  10535  gchen1  10620  fpwwe2lem6  10631  fpwwe2lem10  10635  fpwwe2lem11  10636  prlem936  11042  muladd  11646  leord1  11741  eqord1  11742  ltord2  11743  leord2  11744  eqord2  11745  divadddiv  11929  ltmul12a  12070  lemul12b  12071  fimaxre  12158  supadd  12182  supmullem1  12184  cju  12208  zextlt  12636  zmax  12929  xrre  13148  supxr  13292  ixxdisj  13339  iooshf  13403  icodisj  13453  ioojoin  13460  iccshftr  13463  iccshftl  13465  iccdil  13467  icccntr  13469  iccf1o  13473  fzaddel  13535  fzsubel  13537  modadd1  13873  modmul1  13889  seqcaopr  14005  expsub  14076  expmordi  14132  sqlecan  14173  facndiv  14248  hashss  14369  hashfacen  14413  hashfacenOLD  14414  hashf1lem1  14415  hashf1lem1OLD  14416  fi1uzind  14458  brfi1indALT  14461  ccatpfx  14651  swrdccatfn  14674  swrdccatin2  14679  2cshwcshw  14776  resqrex  15197  fprodeq0  15919  lcmdvds  16545  hashdvds  16708  eulerthlem2  16715  pceu  16779  pcqcl  16789  infpnlem1  16843  4sqlem11  16888  ramcl  16962  prmgaplem5  16988  imasvscafn  17483  invfun  17711  initoeu2lem2  17965  catcisolem  18060  funcestrcsetclem8  18099  fullestrcsetc  18103  embedsetcestrclem  18109  funcsetcestrclem8  18114  fullsetcestrc  18118  prfcl  18155  prf1st  18156  prf2nd  18157  1st2ndprf  18158  curfuncf  18191  ipodrsfi  18492  mhmpropd  18678  subsubm  18697  pwsdiagmhm  18712  frmdgsum  18743  grplcan  18885  grplmulf1o  18897  dfgrp3lem  18921  mulgsubcl  18968  subsubg  19029  eqger  19058  qus0subgadd  19076  resghm  19108  conjghm  19123  orbsta  19177  psgnunilem2  19363  odmulg  19424  sylow2a  19487  sylow3lem1  19495  lsmssv  19511  pj1ghm  19571  frgpup1  19643  ghmplusg  19714  subsubrg  20345  issrngd  20469  lmhmco  20654  lmhmf1o  20657  lmhmima  20658  lmhmpreima  20659  reslmhm  20663  pwsdiaglmhm  20668  pwssplit2  20671  pwssplit3  20672  pj1lmhm  20711  lspdisj  20738  prmirred  21044  cygznlem3  21125  frlmsslsp  21351  frlmlbs  21352  frlmup1  21353  issubassa2  21446  psrbagconf1o  21489  psrbagconf1oOLD  21490  psrgrp  21517  evlslem2  21642  evlslem1  21645  ply1sclf1  21811  mamuass  21902  dmatmul  21999  dmatsubcl  22000  dmatmulcl  22002  dmatcrng  22004  scmatcrng  22023  mdetunilem9  22122  pm2mpghm  22318  fvmptnn04ifb  22353  toponmre  22597  neiptopreu  22637  ordtbas  22696  txcls  23108  txlm  23152  qtoptop2  23203  qtoprest  23221  kqt0lem  23240  ptuncnv  23311  fmfnfmlem4  23461  alexsubALTlem2  23552  tgpmulg  23597  blin  23927  xmeter  23939  xmetresbl  23943  dscmet  24081  nmdvr  24187  metnrmlem3  24377  icccvx  24466  bndth  24474  htpycc  24496  pcohtpylem  24535  pi1blem  24555  lmmbrf  24779  iscfil2  24783  iscau4  24796  minveclem7  24952  elovolm  24992  dyaddisjlem  25112  ismbfd  25156  itg1mulc  25222  dvlip  25510  dvcvx  25537  plypf1  25726  eff1olem  26057  logccv  26171  lawcos  26321  leibpilem1  26445  sqff1o  26686  dvdsppwf1o  26690  dvdsflf1o  26691  fsumdvdsmul  26699  sgmmul  26704  fsumvma  26716  bposlem6  26792  lgsdchr  26858  rpvmasum2  27015  pntpbnd1  27089  ostthlem1  27130  sltres  27165  nodenselem5  27191  nodenselem6  27192  nodense  27195  addsproplem2  27456  mulsuniflem  27607  precsexlem9  27664  precsexlem10  27665  precsexlem11  27666  tgbtwntriv2  27769  ercgrg  27799  hlpasch  28038  colinearalglem4  28198  axlowdimlem15  28245  axcontlem7  28259  axcontlem8  28260  axcontlem10  28262  usgr1v  28544  pthdivtx  29017  clwwlkn1loopb  29327  grpolcan  29814  nvmf  29929  sspmval  30017  nmosetre  30048  minvecolem7  30167  hiassdi  30375  shscli  30601  fh1  30902  fh2  30903  cm2j  30904  chscllem2  30922  spansncvi  30936  5oalem2  30939  adjsym  31117  nmopsetretALT  31147  nmfnsetre  31161  cnvadj  31176  cnvunop  31202  unoplin  31204  hmoplin  31226  lnopmi  31284  hmops  31304  hmopm  31305  nmcexi  31310  adjlnop  31370  adjmul  31376  adjadd  31377  opsqrlem1  31424  mdsl0  31594  ssmd2  31596  mdexchi  31619  superpos  31638  chrelat2i  31649  atcvatlem  31669  atcvati  31670  chirredlem1  31674  chirredi  31678  atcvat3i  31680  atcvat4i  31681  mdsymlem3  31689  mdsymlem5  31691  cdj3lem2b  31721  ifnebib  31812  isoun  31954  xrge0infss  32004  extdg1id  32773  ddemeas  33265  fsum2dsub  33650  hgt750lemb  33699  bnj1145  34035  subfacp1lem3  34204  subfacp1lem5  34206  satfv1lem  34384  btwnconn1lem12  35101  colinbtwnle  35121  broutsideof2  35125  lineelsb2  35151  nn0prpwlem  35255  neibastop2lem  35293  tailfb  35310  onsuct0  35374  finxpreclem2  36319  lindsenlbs  36531  poimirlem4  36540  poimirlem26  36562  poimirlem27  36563  poimirlem31  36567  heicant  36571  mblfinlem2  36574  mblfinlem3  36575  ismblfin  36577  ftc1anclem5  36613  ftc1anclem6  36614  ftc1anc  36617  sdclem1  36659  seqpo  36663  sstotbnd  36691  cntotbnd  36712  ismtycnv  36718  ismtyres  36724  heibor  36737  exidreslem  36793  ghomdiv  36808  grpokerinj  36809  rngohomco  36890  rngoisoco  36898  idlsubcl  36939  divrngidl  36944  ispridl2  36954  ispridlc  36986  riotasv3d  37878  omllaw3  38163  omlfh1N  38176  hlrelat2  38322  cvratlem  38340  cvrat  38341  cvrat3  38361  cvrat4  38362  ps-2  38397  elpaddn0  38719  paddss12  38738  pmodlem2  38766  cdleme0cq  39134  cdlemeg49lebilem  39458  cdleme50eq  39460  tendoeq2  39693  tendoex  39894  diameetN  39975  diainN  39976  dvhopN  40035  djajN  40056  dihmeetcl  40264  mapdheq2  40648  3factsumint1  40934  metakunt16  41048  imacrhmcl  41137  evlsvvval  41183  evlselvlem  41206  fsuppind  41210  0prjspn  41418  fphpdo  41603  pell1234qrne0  41639  pell14qrgt0  41645  pell1qrge1  41656  monotoddzzfi  41729  jm2.18  41775  wepwsolem  41832  dnnumch3  41837  dnwech  41838  kelac1  41853  kercvrlsm  41873  onov0suclim  42072  cantnfresb  42122  dssmapnvod  42819  gsumws3  42996  gsumws4  42997  mnuprdlem1  43079  mnuprdlem2  43080  cncmpmax  43764  fiiuncl  43800  choicefi  43947  fvelima2  44012  mullimc  44380  mullimcf  44387  idlimc  44390  limclner  44415  climleltrp  44440  limsupub  44468  climuzlem  44507  climliminflimsup2  44573  xlimbr  44591  xlimxrre  44595  dfxlim2v  44611  fperdvper  44683  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  dvnprodlem1  44710  stoweidlem27  44791  stoweidlem48  44812  fourierdlem42  44913  fourierdlem63  44933  fourierdlem65  44935  dfsalgen2  45105  subsaliuncl  45122  sge0iunmptlemfi  45177  sge0rpcpnf  45185  iundjiun  45224  psmeasure  45235  ovnsubaddlem2  45335  hoidmvle  45364  ovolval4lem2  45414  smflimlem2  45536  smflimlem3  45537  smflimlem6  45540  smflimmpt  45574  fcoresf1  45827  icceuelpart  46152  mgmhmpropd  46603  subsubmgm  46615  subsubrng  46790  rngqiprngghmlem2  46821  rngqiprngghm  46832  srhmsubc  47022  srhmsubcALTV  47040  catprs  47679