Theorem adantrl 729

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad2ant2l  759  ad2ant2rl  762  cases2ALT  1064  consensus  1068  3ad2antr2  1208  3ad2antr3  1209  po2ne  5587  opabssxpd  5710  frpoind  6347  ordelord  6386  f1un  6845  fvelima2  6937  f1cofveqaeqALT  7258  isocnv  7334  isores2  7337  f1oiso2  7356  offval  7689  ordsucun  7823  xp2nd  8021  2ndconst  8098  sexp2  8144  smoord  8354  tfrlem9  8374  tfrlem11  8377  oaass  8548  omordi  8553  omwordri  8559  odi  8566  oewordri  8580  nnawordi  8609  nnmordi  8619  coflton  8659  dom2lem  8991  fundmen  9031  sbthlem9  9086  mapen  9132  mapunen  9137  ssenen  9142  domfi  9176  mapfien  9371  inf3lem6  9605  ttrclselem2  9698  frind  9725  r1val1  9761  rankval3b  9801  numacn  10045  infxpabs  10206  infxp  10209  cfsmolem  10265  infpssrlem4  10301  fin23lem27  10323  isf34lem4  10372  hsmexlem2  10422  axdc3lem2  10446  axdc3lem4  10448  iundom2g  10535  gchen1  10621  fpwwe2lem6  10632  fpwwe2lem10  10636  fpwwe2lem11  10637  prlem936  11043  muladd  11657  leord1  11752  eqord1  11753  ltord2  11754  leord2  11755  eqord2  11756  divadddiv  11941  ltmul12a  12082  lemul12b  12083  fimaxre  12170  supadd  12194  supmullem1  12196  cju  12225  zextlt  12682  zmax  12981  xrre  13207  supxr  13351  ixxdisj  13399  iooshf  13465  icodisj  13515  ioojoin  13522  iccshftr  13525  iccshftl  13527  iccdil  13529  icccntr  13531  iccf1o  13535  fzaddel  13599  fzsubel  13601  modadd1  13955  modmul1  13974  seqcaopr  14089  expsub  14160  expmordi  14217  sqlecan  14259  facndiv  14338  hashss  14459  hashfacen  14505  hashf1lem1  14506  fi1uzind  14558  brfi1indALT  14561  ccatpfx  14756  swrdccatfn  14779  swrdccatin2  14784  2cshwcshw  14882  resqrex  15321  fprodeq0  16048  lcmdvds  16684  hashdvds  16852  eulerthlem2  16859  pceu  16924  pcqcl  16934  infpnlem1  16988  4sqlem11  17033  ramcl  17107  prmgaplem5  17133  imasvscafn  17609  invfun  17839  initoeu2lem2  18090  catcisolem  18185  funcestrcsetclem8  18221  fullestrcsetc  18225  embedsetcestrclem  18231  funcsetcestrclem8  18236  fullsetcestrc  18240  prfcl  18277  prf1st  18278  prf2nd  18279  1st2ndprf  18280  curfuncf  18312  ipodrsfi  18613  mgmhmpropd  18778  subsubmgm  18790  mhmpropd  18874  subsubm  18899  pwsdiagmhm  18914  frmdgsum  18945  grplcan  19091  grplmulf1o  19103  grpraddf1o  19104  dfgrp3lem  19128  mulgsubcl  19178  subsubg  19240  eqger  19270  qus0subgadd  19294  resghm  19326  conjghm  19343  orbsta  19407  psgnunilem2  19589  odmulg  19650  sylow2a  19713  sylow3lem1  19721  lsmssv  19737  pj1ghm  19797  frgpup1  19869  ghmplusg  19940  subsubrng  20692  subsubrg  20727  srhmsubc  20809  issrngd  20988  lmhmco  21194  lmhmf1o  21197  lmhmima  21198  lmhmpreima  21199  reslmhm  21203  pwsdiaglmhm  21208  pwssplit2  21211  pwssplit3  21212  pj1lmhm  21251  lspdisj  21279  rngqiprngghmlem2  21458  rngqiprngghm  21469  prmirred  21654  cygznlem3  21749  frlmsslsp  21976  frlmlbs  21977  frlmup1  21978  issubassa2  22072  psrbagconf1o  22109  psrgrp  22136  evlslem2  22260  evlslem1  22263  evlsvvval  22274  ply1sclf1  22480  mamuass  22589  dmatmul  22684  dmatsubcl  22685  dmatmulcl  22687  dmatcrng  22689  scmatcrng  22708  mdetunilem9  22807  pm2mpghm  23003  fvmptnn04ifb  23038  toponmre  23280  neiptopreu  23320  ordtbas  23379  txcls  23792  txlm  23836  qtoptop2  23887  qtoprest  23905  kqt0lem  23924  ptuncnv  23995  fmfnfmlem4  24145  alexsubALTlem2  24236  tgpmulg  24281  blin  24609  xmeter  24621  xmetresbl  24625  dscmet  24760  nmdvr  24858  metnrmlem3  25050  icccvx  25140  bndth  25148  htpycc  25170  pcohtpylem  25209  pi1blem  25229  lmmbrf  25452  iscfil2  25456  iscau4  25469  minveclem7  25625  elovolm  25665  dyaddisjlem  25785  ismbfd  25829  itg1mulc  25894  dvlip  26183  dvcvx  26210  plypf1  26400  eff1olem  26744  logccv  26859  lawcos  27012  leibpilem1  27136  sqff1o  27377  dvdsppwf1o  27381  dvdsflf1o  27382  fsumdvdsmul  27390  sgmmul  27396  fsumvma  27408  bposlem6  27484  lgsdchr  27550  rpvmasum2  27707  pntpbnd1  27781  ostthlem1  27822  ltsres  27857  nodenselem5  27883  nodenselem6  27884  nodense  27887  addsproplem2  28194  mulsuniflem  28373  mulsunif2lem  28393  precsexlem9  28439  precsexlem10  28440  precsexlem11  28441  om2noseqlt2  28524  om2noseqf1o  28525  z12sge0  28707  elreno2  28719  tgbtwntriv2  28787  ercgrg  28817  hlpasch  29069  colinearalglem4  29290  axlowdimlem15  29337  axcontlem7  29351  axcontlem8  29352  axcontlem10  29354  usgr1v  29640  pthdivtx  30115  clwwlkn1loopb  30437  grpolcan  30929  nvmf  31044  sspmval  31132  nmosetre  31163  minvecolem7  31282  hiassdi  31490  shscli  31716  fh1  32017  fh2  32018  cm2j  32019  chscllem2  32037  spansncvi  32051  5oalem2  32054  adjsym  32232  nmopsetretALT  32262  nmfnsetre  32276  cnvadj  32291  cnvunop  32317  unoplin  32319  hmoplin  32341  lnopmi  32399  hmops  32419  hmopm  32420  nmcexi  32425  adjlnop  32485  adjmul  32491  adjadd  32492  opsqrlem1  32539  mdsl0  32709  ssmd2  32711  mdexchi  32734  superpos  32753  chrelat2i  32764  atcvatlem  32784  atcvati  32785  chirredlem1  32789  chirredi  32793  atcvat3i  32795  atcvat4i  32796  mdsymlem3  32804  mdsymlem5  32806  cdj3lem2b  32836  ifnebib  32942  isoun  33094  xrge0infss  33151  1arithufdlem3  33876  extdg1id  34096  ddemeas  34667  fsum2dsub  35035  hgt750lemb  35084  bnj1145  35422  subfacp1lem3  35687  subfacp1lem5  35689  cvxpconn  35747  satfv1lem  35867  btwnconn1lem12  36603  colinbtwnle  36623  broutsideof2  36627  lineelsb2  36653  nadddilem2  36726  nadddilem4  36728  nn0prpwlem  36866  neibastop2lem  36904  tailfb  36921  onsuct0  36985  finxpreclem2  38069  lindsenlbs  38299  poimirlem4  38308  poimirlem26  38330  poimirlem27  38331  poimirlem31  38335  heicant  38339  mblfinlem2  38342  mblfinlem3  38343  ismblfin  38345  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anc  38385  sdclem1  38427  seqpo  38431  sstotbnd  38459  cntotbnd  38480  ismtycnv  38486  ismtyres  38492  heibor  38505  exidreslem  38561  ghomdiv  38576  grpokerinj  38577  rngohomco  38658  rngoisoco  38666  idlsubcl  38707  divrngidl  38712  ispridl2  38722  ispridlc  38754  riotasv3d  39767  omllaw3  40052  omlfh1N  40065  hlrelat2  40210  cvratlem  40228  cvrat  40229  cvrat3  40249  cvrat4  40250  ps-2  40285  elpaddn0  40607  paddss12  40626  pmodlem2  40654  cdleme0cq  41022  cdlemeg49lebilem  41346  cdleme50eq  41348  tendoeq2  41581  tendoex  41782  diameetN  41863  diainN  41864  dvhopN  41923  djajN  41944  dihmeetcl  42152  mapdheq2  42536  3factsumint1  42821  imacrhmcl  43321  psrmnd  43344  evlselvlem  43353  fsuppind  43355  0prjspn  43393  fphpdo  43577  pell1234qrne0  43613  pell14qrgt0  43619  pell1qrge1  43630  monotoddzzfi  43702  jm2.18  43748  wepwsolem  43802  dnnumch3  43807  dnwech  43808  kelac1  43823  kercvrlsm  43843  onov0suclim  44034  cantnfresb  44084  dssmapnvod  44779  gsumws3  44955  gsumws4  44956  mnuprdlem1  45015  mnuprdlem2  45016  traxext  45719  modelac8prim  45734  cncmpmax  45785  fiiuncl  45818  choicefi  45950  mullimc  46365  mullimcf  46372  idlimc  46375  limclner  46398  climleltrp  46423  limsupub  46451  climuzlem  46490  climliminflimsup2  46556  xlimbr  46574  xlimxrre  46578  dfxlim2v  46594  fperdvper  46666  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvnprodlem1  46693  stoweidlem27  46774  stoweidlem48  46795  fourierdlem42  46896  fourierdlem63  46916  fourierdlem65  46918  dfsalgen2  47088  subsaliuncl  47105  sge0iunmptlemfi  47160  sge0rpcpnf  47168  iundjiun  47207  psmeasure  47218  ovnsubaddlem2  47318  hoidmvle  47347  ovolval4lem2  47397  smflimlem2  47519  smflimlem3  47520  smflimlem6  47523  smflimmpt  47557  fcoresf1  47839  icceuelpart  48218  gpgedgvtx0  48859  gpgedgvtx1  48860  srhmsubcALTV  49123  catprs  49822  thincciso2  50266  functermclem  50318  functermc  50319  fulltermc  50322