Theorem adantrl 703

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  ad2ant2l  733  ad2ant2rl  736  cases2ALT  1029  consensus  1033  3ad2antr2  1169  3ad2antr3  1170  po2ne  5341  opabssxpd  5636  wfi  6019  ordelord  6051  foco  6431  f1cofveqaeqALT  6842  isocnv  6906  isores2  6909  f1oiso2  6928  offval  7234  ordsucun  7356  xp2nd  7534  2ndconst  7604  wfrdmcl  7767  smoord  7806  tfrlem9  7825  tfrlem11  7828  oaass  7988  omordi  7993  omwordri  7999  odi  8006  oewordri  8019  nnawordi  8048  nnmordi  8058  dom2lem  8346  fundmen  8380  sbthlem9  8431  mapen  8477  mapunen  8482  ssenen  8487  domfi  8534  mapfien  8666  inf3lem6  8890  r1val1  9009  rankval3b  9049  numacn  9269  infxpabs  9432  infxp  9435  cfsmolem  9490  infpssrlem4  9526  fin23lem27  9548  isf34lem4  9597  hsmexlem2  9647  axdc3lem2  9671  axdc3lem4  9673  iundom2g  9760  gchen1  9845  fpwwe2lem7  9856  fpwwe2lem11  9860  fpwwe2lem12  9861  prlem936  10267  muladd  10873  leord1  10968  eqord1  10969  ltord2  10970  leord2  10971  eqord2  10972  divadddiv  11156  ltmul12a  11297  lemul12b  11298  fimaxre  11385  supadd  11410  supmullem1  11412  cju  11435  zextlt  11869  zmax  12159  xrre  12379  supxr  12522  ixxdisj  12569  iooshf  12631  icodisj  12678  ioojoin  12685  iccshftr  12688  iccshftl  12690  iccdil  12692  icccntr  12694  iccf1o  12698  fzaddel  12757  fzsubel  12759  modadd1  13091  modmul1  13107  seqcaopr  13222  expsub  13292  expmordi  13346  sqlecan  13386  facndiv  13463  hashss  13583  hashfacen  13625  hashf1lem1  13626  fi1uzind  13666  brfi1indALT  13669  swrdccatin12lem2bOLD  13928  2cshwcshw  14049  resqrex  14471  fprodeq0  15189  lcmdvds  15808  hashdvds  15968  eulerthlem2  15975  pceu  16039  pcqcl  16049  infpnlem1  16102  4sqlem11  16147  ramcl  16221  prmgaplem5  16247  imasvscafn  16666  invfun  16892  initoeu2lem2  17133  catcisolem  17224  funcestrcsetclem8  17255  fullestrcsetc  17259  embedsetcestrclem  17265  funcsetcestrclem8  17270  fullsetcestrc  17274  prfcl  17311  prf1st  17312  prf2nd  17313  1st2ndprf  17314  curfuncf  17346  ipodrsfi  17631  mhmpropd  17809  subsubm  17825  pwsdiagmhm  17837  gsumccat  17846  frmdgsum  17868  grplcan  17948  grplmulf1o  17960  dfgrp3lem  17984  mulgsubcl  18027  subsubg  18086  eqger  18113  resghm  18145  conjghm  18160  orbsta  18214  psgnunilem2  18385  odmulg  18444  sylow2a  18505  sylow3lem1  18513  lsmssv  18529  pj1ghm  18587  frgpup1  18661  ghmplusg  18722  subsubrg  19284  issrngd  19354  lmhmco  19537  lmhmf1o  19540  lmhmima  19541  lmhmpreima  19542  reslmhm  19546  pwsdiaglmhm  19551  pwssplit2  19554  pwssplit3  19555  pj1lmhm  19594  lspdisj  19619  issubassa2  19839  psrbagconf1o  19868  evlslem2  20005  evlslem1  20008  ply1sclf1  20160  prmirred  20344  cygznlem3  20418  frlmsslsp  20642  frlmlbs  20643  frlmup1  20644  mamuass  20715  dmatmul  20810  dmatsubcl  20811  dmatmulcl  20813  dmatcrng  20815  scmatcrng  20834  mdetunilem9  20933  pm2mpghm  21128  fvmptnn04ifb  21163  toponmre  21405  neiptopreu  21445  ordtbas  21504  txcls  21916  txlm  21960  qtoptop2  22011  qtoprest  22029  kqt0lem  22048  ptuncnv  22119  fmfnfmlem4  22269  alexsubALTlem2  22360  tgpmulg  22405  blin  22734  xmeter  22746  xmetresbl  22750  dscmet  22885  nmdvr  22982  metnrmlem3  23172  icccvx  23257  bndth  23265  htpycc  23287  pcohtpylem  23326  pi1blem  23346  lmmbrf  23568  iscfil2  23572  iscau4  23585  minveclem7  23741  elovolm  23779  dyaddisjlem  23899  ismbfd  23943  itg1mulc  24008  dvlip  24293  dvcvx  24320  plypf1  24505  eff1olem  24833  logccv  24947  lawcos  25095  leibpilem1  25219  sqff1o  25461  dvdsppwf1o  25465  dvdsflf1o  25466  fsumdvdsmul  25474  sgmmul  25479  fsumvma  25491  bposlem6  25567  lgsdchr  25633  rpvmasum2  25790  pntpbnd1  25864  ostthlem1  25905  tgbtwntriv2  25975  ercgrg  26005  hlpasch  26244  colinearalglem4  26398  axlowdimlem15  26445  axcontlem7  26459  axcontlem8  26460  axcontlem10  26462  usgr1v  26741  pthdivtx  27218  clwwlkn1loopb  27559  grpolcan  28084  nvmf  28199  sspmval  28287  nmosetre  28318  sspphOLD  28409  minvecolem7  28438  hiassdi  28647  shscli  28875  fh1  29176  fh2  29177  cm2j  29178  chscllem2  29196  spansncvi  29210  5oalem2  29213  adjsym  29391  nmopsetretALT  29421  nmfnsetre  29435  cnvadj  29450  cnvunop  29476  unoplin  29478  hmoplin  29500  lnopmi  29558  hmops  29578  hmopm  29579  nmcexi  29584  adjlnop  29644  adjmul  29650  adjadd  29651  opsqrlem1  29698  mdsl0  29868  ssmd2  29870  mdexchi  29893  superpos  29912  chrelat2i  29923  atcvatlem  29943  atcvati  29944  chirredlem1  29948  chirredi  29952  atcvat3i  29954  atcvat4i  29955  mdsymlem3  29963  mdsymlem5  29965  cdj3lem2b  29995  isoun  30189  xrge0infss  30236  extdg1id  30679  ddemeas  31137  fsum2dsub  31523  hgt750lemb  31572  bnj1145  31907  subfacp1lem3  32011  subfacp1lem5  32013  frpoind  32598  frind  32603  sltres  32687  nodenselem5  32710  nodenselem6  32711  nodense  32714  btwnconn1lem12  33077  colinbtwnle  33097  broutsideof2  33101  lineelsb2  33127  nn0prpwlem  33188  neibastop2lem  33226  tailfb  33243  onsuct0  33306  finxpreclem2  34109  lindsenlbs  34325  poimirlem4  34334  poimirlem26  34356  poimirlem27  34357  poimirlem31  34361  heicant  34365  mblfinlem2  34368  mblfinlem3  34369  ismblfin  34371  ftc1anclem5  34409  ftc1anclem6  34410  ftc1anc  34413  sdclem1  34457  seqpo  34461  sstotbnd  34492  cntotbnd  34513  ismtycnv  34519  ismtyres  34525  heibor  34538  exidreslem  34594  ghomdiv  34609  grpokerinj  34610  rngohomco  34691  rngoisoco  34699  idlsubcl  34740  divrngidl  34745  ispridl2  34755  ispridlc  34787  riotasv3d  35538  omllaw3  35823  omlfh1N  35836  hlrelat2  35981  cvratlem  35999  cvrat  36000  cvrat3  36020  cvrat4  36021  ps-2  36056  elpaddn0  36378  paddss12  36397  pmodlem2  36425  cdleme0cq  36793  cdlemeg49lebilem  37117  cdleme50eq  37119  tendoeq2  37352  tendoex  37553  diameetN  37634  diainN  37635  dvhopN  37694  djajN  37715  dihmeetcl  37923  mapdheq2  38307  0prjspn  38674  fphpdo  38807  pell1234qrne0  38843  pell14qrgt0  38849  pell1qrge1  38860  monotoddzzfi  38932  jm2.18  38978  wepwsolem  39035  dnnumch3  39040  dnwech  39041  kelac1  39056  kercvrlsm  39076  dssmapnvod  39726  gsumws3  39911  gsumws4  39912  mnuprdlem1  39980  mnuprdlem2  39981  cncmpmax  40705  fiiuncl  40744  choicefi  40886  fvelima2  40958  mullimc  41326  mullimcf  41333  idlimc  41336  limclner  41361  climleltrp  41386  limsupub  41414  climuzlem  41453  climliminflimsup2  41519  xlimbr  41537  xlimxrre  41541  dfxlim2v  41557  fperdvper  41631  ioodvbdlimc1lem2  41645  ioodvbdlimc2lem  41647  dvnprodlem1  41659  stoweidlem27  41741  stoweidlem48  41762  fourierdlem42  41863  fourierdlem63  41883  fourierdlem65  41885  dfsalgen2  42053  subsaliuncl  42070  sge0iunmptlemfi  42124  sge0rpcpnf  42132  iundjiun  42171  psmeasure  42182  ovnsubaddlem2  42282  hoidmvle  42311  ovolval4lem2  42361  ovolval5lem3  42365  smflimlem2  42477  smflimlem3  42478  smflimlem6  42481  smflimmpt  42513  icceuelpart  42966  mgmhmpropd  43418  subsubmgm  43430  srhmsubc  43709  srhmsubcALTV  43727