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  5574  opabssxpd  5697  frpoind  6347  ordelord  6386  f1un  6848  fvelima2  6940  f1cofveqaeqALT  7264  isocnv  7340  isores2  7343  f1oiso2  7362  offval  7704  ordsucun  7838  xp2nd  8036  2ndconst  8116  sexp2  8167  smoord  8378  tfrlem9  8398  tfrlem11  8401  oaass  8574  omordi  8579  omwordri  8585  odi  8592  oewordri  8606  nnawordi  8635  nnmordi  8645  coflton  8685  dom2lem  9024  fundmen  9064  sbthlem9  9119  mapen  9165  mapunen  9170  ssenen  9175  domfi  9209  mapfien  9405  inf3lem6  9639  ttrclselem2  9732  frind  9759  r1val1  9798  rankval3b  9841  numacn  10133  infxpabs  10294  infxp  10297  cfsmolem  10353  infpssrlem4  10389  fin23lem27  10411  isf34lem4  10460  hsmexlem2  10510  axdc3lem2  10534  axdc3lem4  10536  iundom2g  10629  gchen1  10715  fpwwe2lem6  10726  fpwwe2lem10  10730  fpwwe2lem11  10731  prlem936  11137  muladd  11753  leord1  11848  eqord1  11849  ltord2  11850  leord2  11851  eqord2  11852  divadddiv  12037  ltmul12a  12178  lemul12b  12179  fimaxre  12266  supadd  12290  supmullem1  12292  cju  12321  zextlt  12778  zmax  13077  xrre  13304  supxr  13448  ixxdisj  13496  iooshf  13562  icodisj  13612  ioojoin  13619  iccshftr  13622  iccshftl  13624  iccdil  13626  icccntr  13628  iccf1o  13632  fzaddel  13697  fzsubel  13699  modadd1  14053  modmul1  14072  seqcaopr  14187  expsub  14258  expmordi  14315  sqlecan  14358  facndiv  14437  hashss  14558  hashfacen  14604  hashf1lem1  14605  fi1uzind  14657  brfi1indALT  14660  ccatpfx  14856  swrdccatfn  14879  swrdccatin2  14884  2cshwcshw  14982  resqrex  15424  fprodeq0  16149  lcmdvds  16790  hashdvds  16959  eulerthlem2  16966  pceu  17031  pcqcl  17041  infpnlem1  17095  4sqlem11  17140  ramcl  17214  prmgaplem5  17240  imasvscafn  17716  invfun  17946  initoeu2lem2  18197  catcisolem  18292  funcestrcsetclem8  18328  fullestrcsetc  18332  embedsetcestrclem  18338  funcsetcestrclem8  18343  fullsetcestrc  18347  prfcl  18384  prf1st  18385  prf2nd  18386  1st2ndprf  18387  curfuncf  18419  ipodrsfi  18720  mgmhmpropd  18894  subsubmgm  18906  mhmpropd  18994  subsubm  19019  pwsdiagmhm  19034  frmdgsum  19065  grplcan  19218  grplmulf1o  19230  grpraddf1o  19231  dfgrp3lem  19255  mulgsubcl  19305  subsubg  19367  eqger  19397  qus0subgadd  19421  resghm  19453  conjghm  19470  orbsta  19534  psgnunilem2  19716  odmulg  19777  sylow2a  19840  sylow3lem1  19848  lsmssv  19864  pj1ghm  19924  frgpup1  19996  ghmplusg  20067  subsubrng  20822  subsubrg  20857  srhmsubc  20939  issrngd  21119  lmhmco  21325  lmhmf1o  21328  lmhmima  21329  lmhmpreima  21330  reslmhm  21334  pwsdiaglmhm  21339  pwssplit2  21342  pwssplit3  21343  pj1lmhm  21382  lspdisj  21410  rngqiprngghmlem2  21591  rngqiprngghm  21602  prmirred  21787  cygznlem3  21882  frlmsslsp  22109  frlmlbs  22110  frlmup1  22111  lindsenlbs  22164  issubassa2  22207  psrbagconf1o  22244  psrgrp  22271  evlslem2  22395  evlslem1  22398  evlsvvval  22409  ply1sclf1  22615  mamuass  22724  dmatmul  22819  dmatsubcl  22820  dmatmulcl  22822  dmatcrng  22824  scmatcrng  22843  mdetunilem9  22942  pm2mpghm  23141  fvmptnn04ifb  23176  toponmre  23418  neiptopreu  23458  ordtbas  23517  txcls  23930  txlm  23974  qtoptop2  24025  qtoprest  24043  kqt0lem  24062  ptuncnv  24133  fmfnfmlem4  24283  alexsubALTlem2  24374  tgpmulg  24419  blin  24747  xmeter  24759  xmetresbl  24763  dscmet  24898  nmdvr  24996  metnrmlem3  25188  icccvx  25278  bndth  25286  htpycc  25308  pcohtpylem  25347  pi1blem  25367  lmmbrf  25590  iscfil2  25594  iscau4  25607  minveclem7  25763  elovolm  25803  dyaddisjlem  25923  ismbfd  25967  itg1mulc  26032  dvlip  26320  dvcvx  26347  plypf1  26538  eff1olem  26883  logccv  26998  lawcos  27151  leibpilem1  27275  sqff1o  27516  dvdsppwf1o  27520  dvdsflf1o  27521  fsumdvdsmul  27529  sgmmul  27535  fsumvma  27547  bposlem6  27623  lgsdchr  27689  rpvmasum2  27846  pntpbnd1  27920  ostthlem1  27961  ltsres  28026  nodenselem5  28052  nodenselem6  28053  nodense  28056  addsproplem2  28363  mulsuniflem  28542  mulsunif2lem  28562  precsexlem9  28608  precsexlem10  28609  precsexlem11  28610  om2noseqlt2  28693  om2noseqf1o  28694  z12sge0  28876  elreno2  28888  tgbtwntriv2  28957  ercgrg  28987  hlpasch  29241  colinearalglem4  29494  axlowdimlem15  29541  axcontlem7  29555  axcontlem8  29556  axcontlem10  29558  usgr1v  29844  pthdivtx  30319  clwwlkn1loopb  30641  grpolcan  31139  nvmf  31254  sspmval  31342  nmosetre  31373  minvecolem7  31492  hiassdi  31700  shscli  31926  fh1  32227  fh2  32228  cm2j  32229  chscllem2  32247  spansncvi  32261  5oalem2  32264  adjsym  32442  nmopsetretALT  32472  nmfnsetre  32486  cnvadj  32501  cnvunop  32527  unoplin  32529  hmoplin  32551  lnopmi  32609  hmops  32629  hmopm  32630  nmcexi  32635  adjlnop  32695  adjmul  32701  adjadd  32702  opsqrlem1  32749  mdsl0  32919  ssmd2  32921  mdexchi  32944  superpos  32963  chrelat2i  32974  atcvatlem  32994  atcvati  32995  chirredlem1  32999  chirredi  33003  atcvat3i  33005  atcvat4i  33006  mdsymlem3  33014  mdsymlem5  33016  cdj3lem2b  33046  ifnebib  33194  isoun  33344  xrge0infss  33400  1arithufdlem3  34126  extdg1id  34346  ddemeas  34917  fsum2dsub  35284  hgt750lemb  35333  bnj1145  35671  brlexod  35940  brr0d  35942  subfacp1lem3  36035  subfacp1lem5  36037  cvxpconn  36095  satfv1lem  36215  btwnconn1lem12  36957  colinbtwnle  36977  broutsideof2  36981  lineelsb2  37007  nadddilem2  37064  nadddilem4  37066  nn0prpwlem  37204  neibastop2lem  37242  tailfb  37259  onsuct0  37323  finxpreclem2  38420  poimirlem4  38649  poimirlem26  38671  poimirlem27  38672  poimirlem31  38676  heicant  38680  mblfinlem2  38683  mblfinlem3  38684  ismblfin  38686  ftc1anclem5  38722  ftc1anclem6  38723  ftc1anc  38726  sdclem1  38784  seqpo  38788  sstotbnd  38816  cntotbnd  38837  ismtycnv  38843  ismtyres  38849  heibor  38862  exidreslem  38918  ghomdiv  38933  grpokerinj  38934  rngohomco  39015  rngoisoco  39023  idlsubcl  39064  divrngidl  39069  ispridl2  39079  ispridlc  39111  riotasv3d  40124  omllaw3  40409  omlfh1N  40422  hlrelat2  40567  cvratlem  40585  cvrat  40586  cvrat3  40606  cvrat4  40607  ps-2  40642  elpaddn0  40964  paddss12  40983  pmodlem2  41011  cdleme0cq  41379  cdlemeg49lebilem  41703  cdleme50eq  41705  tendoeq2  41938  tendoex  42139  diameetN  42220  diainN  42221  dvhopN  42280  djajN  42301  dihmeetcl  42509  mapdheq2  42893  3factsumint1  43178  imacrhmcl  43688  psrmnd  43714  evlselvlem  43723  fsuppind  43725  0prjspn  43771  fphpdo  43931  pell1234qrne0  43967  pell14qrgt0  43973  pell1qrge1  43984  monotoddzzfi  44056  jm2.18  44102  wepwsolem  44156  dnnumch3  44161  dnwech  44162  kelac1  44172  kercvrlsm  44192  onov0suclim  44383  cantnfresb  44433  dssmapnvod  45127  gsumws3  45303  gsumws4  45304  mnuprdlem1  45363  mnuprdlem2  45364  traxext  46074  modelac8prim  46089  cncmpmax  46156  fiiuncl  46189  choicefi  46321  mullimc  46735  mullimcf  46742  idlimc  46745  limclner  46768  climleltrp  46793  limsupub  46821  climuzlem  46860  climliminflimsup2  46926  xlimbr  46944  xlimxrre  46948  dfxlim2v  46964  fperdvper  47036  ioodvbdlimc1lem2  47049  ioodvbdlimc2lem  47051  dvnprodlem1  47063  stoweidlem27  47144  stoweidlem48  47165  fourierdlem42  47266  fourierdlem63  47286  fourierdlem65  47288  dfsalgen2  47458  subsaliuncl  47475  sge0iunmptlemfi  47530  sge0rpcpnf  47538  iundjiun  47577  psmeasure  47588  ovnsubaddlem2  47688  hoidmvle  47717  ovolval4lem2  47767  smflimlem2  47889  smflimlem3  47890  smflimlem6  47893  smflimmpt  47927  fcoresf1  48246  icceuelpart  48625  gpgedgvtx0  49266  gpgedgvtx1  49267  srhmsubcALTV  49529  catprs  50232  thincciso2  50697  functermclem  50749  functermc  50750  fulltermc  50753