Theorem adantrl 728

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad2ant2l  758  ad2ant2rl  761  cases2ALT  1064  consensus  1068  3ad2antr2  1208  3ad2antr3  1209  po2ne  5585  opabssxpd  5708  frpoind  6343  ordelord  6382  f1un  6841  fvelima2  6933  f1cofveqaeqALT  7256  isocnv  7328  isores2  7331  f1oiso2  7350  offval  7683  ordsucun  7817  xp2nd  8015  2ndconst  8092  sexp2  8138  smoord  8348  tfrlem9  8368  tfrlem11  8371  oaass  8542  omordi  8547  omwordri  8553  odi  8560  oewordri  8574  nnawordi  8603  nnmordi  8613  coflton  8653  dom2lem  8985  fundmen  9024  sbthlem9  9079  mapen  9125  mapunen  9130  ssenen  9135  domfi  9169  mapfien  9364  inf3lem6  9598  ttrclselem2  9691  frind  9718  r1val1  9754  rankval3b  9794  numacn  10029  infxpabs  10190  infxp  10193  cfsmolem  10249  infpssrlem4  10285  fin23lem27  10307  isf34lem4  10356  hsmexlem2  10406  axdc3lem2  10430  axdc3lem4  10432  iundom2g  10519  gchen1  10605  fpwwe2lem6  10616  fpwwe2lem10  10620  fpwwe2lem11  10621  prlem936  11027  muladd  11641  leord1  11736  eqord1  11737  ltord2  11738  leord2  11739  eqord2  11740  divadddiv  11925  ltmul12a  12066  lemul12b  12067  fimaxre  12154  supadd  12178  supmullem1  12180  cju  12209  zextlt  12665  zmax  12964  xrre  13190  supxr  13334  ixxdisj  13382  iooshf  13448  icodisj  13498  ioojoin  13505  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  iccf1o  13518  fzaddel  13582  fzsubel  13584  modadd1  13937  modmul1  13956  seqcaopr  14071  expsub  14142  expmordi  14199  sqlecan  14241  facndiv  14320  hashss  14441  hashfacen  14487  hashf1lem1  14488  fi1uzind  14540  brfi1indALT  14543  ccatpfx  14734  swrdccatfn  14757  swrdccatin2  14762  2cshwcshw  14858  resqrex  15297  fprodeq0  16025  lcmdvds  16661  hashdvds  16829  eulerthlem2  16836  pceu  16901  pcqcl  16911  infpnlem1  16965  4sqlem11  17010  ramcl  17084  prmgaplem5  17110  imasvscafn  17586  invfun  17816  initoeu2lem2  18067  catcisolem  18162  funcestrcsetclem8  18198  fullestrcsetc  18202  embedsetcestrclem  18208  funcsetcestrclem8  18213  fullsetcestrc  18217  prfcl  18254  prf1st  18255  prf2nd  18256  1st2ndprf  18257  curfuncf  18289  ipodrsfi  18590  mgmhmpropd  18751  subsubmgm  18763  mhmpropd  18845  subsubm  18870  pwsdiagmhm  18885  frmdgsum  18916  grplcan  19062  grplmulf1o  19074  grpraddf1o  19075  dfgrp3lem  19099  mulgsubcl  19149  subsubg  19211  eqger  19241  qus0subgadd  19265  resghm  19297  conjghm  19314  orbsta  19378  psgnunilem2  19560  odmulg  19621  sylow2a  19684  sylow3lem1  19692  lsmssv  19708  pj1ghm  19768  frgpup1  19840  ghmplusg  19911  subsubrng  20662  subsubrg  20697  srhmsubc  20779  issrngd  20958  lmhmco  21164  lmhmf1o  21167  lmhmima  21168  lmhmpreima  21169  reslmhm  21173  pwsdiaglmhm  21178  pwssplit2  21181  pwssplit3  21182  pj1lmhm  21221  lspdisj  21249  rngqiprngghmlem2  21428  rngqiprngghm  21439  prmirred  21624  cygznlem3  21719  frlmsslsp  21946  frlmlbs  21947  frlmup1  21948  issubassa2  22042  psrbagconf1o  22079  psrgrp  22106  evlslem2  22230  evlslem1  22233  evlsvvval  22244  ply1sclf1  22450  mamuass  22559  dmatmul  22654  dmatsubcl  22655  dmatmulcl  22657  dmatcrng  22659  scmatcrng  22678  mdetunilem9  22777  pm2mpghm  22973  fvmptnn04ifb  23008  toponmre  23250  neiptopreu  23290  ordtbas  23349  txcls  23761  txlm  23805  qtoptop2  23856  qtoprest  23874  kqt0lem  23893  ptuncnv  23964  fmfnfmlem4  24114  alexsubALTlem2  24205  tgpmulg  24250  blin  24578  xmeter  24590  xmetresbl  24594  dscmet  24729  nmdvr  24827  metnrmlem3  25019  icccvx  25109  bndth  25117  htpycc  25139  pcohtpylem  25178  pi1blem  25198  lmmbrf  25421  iscfil2  25425  iscau4  25438  minveclem7  25594  elovolm  25634  dyaddisjlem  25754  ismbfd  25798  itg1mulc  25863  dvlip  26152  dvcvx  26179  plypf1  26369  eff1olem  26713  logccv  26828  lawcos  26981  leibpilem1  27105  sqff1o  27346  dvdsppwf1o  27350  dvdsflf1o  27351  fsumdvdsmul  27359  sgmmul  27365  fsumvma  27377  bposlem6  27453  lgsdchr  27519  rpvmasum2  27676  pntpbnd1  27750  ostthlem1  27791  ltsres  27826  nodenselem5  27852  nodenselem6  27853  nodense  27856  addsproplem2  28163  mulsuniflem  28342  mulsunif2lem  28362  precsexlem9  28408  precsexlem10  28409  precsexlem11  28410  om2noseqlt2  28493  om2noseqf1o  28494  z12sge0  28676  elreno2  28688  tgbtwntriv2  28756  ercgrg  28786  hlpasch  29038  colinearalglem4  29259  axlowdimlem15  29306  axcontlem7  29320  axcontlem8  29321  axcontlem10  29323  usgr1v  29606  pthdivtx  30076  clwwlkn1loopb  30394  grpolcan  30882  nvmf  30997  sspmval  31085  nmosetre  31116  minvecolem7  31235  hiassdi  31443  shscli  31669  fh1  31970  fh2  31971  cm2j  31972  chscllem2  31990  spansncvi  32004  5oalem2  32007  adjsym  32185  nmopsetretALT  32215  nmfnsetre  32229  cnvadj  32244  cnvunop  32270  unoplin  32272  hmoplin  32294  lnopmi  32352  hmops  32372  hmopm  32373  nmcexi  32378  adjlnop  32438  adjmul  32444  adjadd  32445  opsqrlem1  32492  mdsl0  32662  ssmd2  32664  mdexchi  32687  superpos  32706  chrelat2i  32717  atcvatlem  32737  atcvati  32738  chirredlem1  32742  chirredi  32746  atcvat3i  32748  atcvat4i  32749  mdsymlem3  32757  mdsymlem5  32759  cdj3lem2b  32789  ifnebib  32895  isoun  33047  xrge0infss  33105  1arithufdlem3  33836  extdg1id  34056  ddemeas  34626  fsum2dsub  34994  hgt750lemb  35043  bnj1145  35381  subfacp1lem3  35674  subfacp1lem5  35676  cvxpconn  35734  satfv1lem  35854  btwnconn1lem12  36590  colinbtwnle  36610  broutsideof2  36614  lineelsb2  36640  nn0prpwlem  36833  neibastop2lem  36871  tailfb  36888  onsuct0  36952  finxpreclem2  38036  lindsenlbs  38266  poimirlem4  38275  poimirlem26  38297  poimirlem27  38298  poimirlem31  38302  heicant  38306  mblfinlem2  38309  mblfinlem3  38310  ismblfin  38312  ftc1anclem5  38348  ftc1anclem6  38349  ftc1anc  38352  sdclem1  38394  seqpo  38398  sstotbnd  38426  cntotbnd  38447  ismtycnv  38453  ismtyres  38459  heibor  38472  exidreslem  38528  ghomdiv  38543  grpokerinj  38544  rngohomco  38625  rngoisoco  38633  idlsubcl  38674  divrngidl  38679  ispridl2  38689  ispridlc  38721  riotasv3d  39734  omllaw3  40019  omlfh1N  40032  hlrelat2  40177  cvratlem  40195  cvrat  40196  cvrat3  40216  cvrat4  40217  ps-2  40252  elpaddn0  40574  paddss12  40593  pmodlem2  40621  cdleme0cq  40989  cdlemeg49lebilem  41313  cdleme50eq  41315  tendoeq2  41548  tendoex  41749  diameetN  41830  diainN  41831  dvhopN  41890  djajN  41911  dihmeetcl  42119  mapdheq2  42503  3factsumint1  42788  imacrhmcl  43288  psrmnd  43311  evlselvlem  43320  fsuppind  43322  0prjspn  43360  fphpdo  43544  pell1234qrne0  43580  pell14qrgt0  43586  pell1qrge1  43597  monotoddzzfi  43669  jm2.18  43715  wepwsolem  43769  dnnumch3  43774  dnwech  43775  kelac1  43790  kercvrlsm  43810  onov0suclim  44001  cantnfresb  44051  dssmapnvod  44746  gsumws3  44922  gsumws4  44923  mnuprdlem1  44982  mnuprdlem2  44983  traxext  45686  modelac8prim  45701  cncmpmax  45752  fiiuncl  45785  choicefi  45917  mullimc  46332  mullimcf  46339  idlimc  46342  limclner  46365  climleltrp  46390  limsupub  46418  climuzlem  46457  climliminflimsup2  46523  xlimbr  46541  xlimxrre  46545  dfxlim2v  46561  fperdvper  46633  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  dvnprodlem1  46660  stoweidlem27  46741  stoweidlem48  46762  fourierdlem42  46863  fourierdlem63  46883  fourierdlem65  46885  dfsalgen2  47055  subsaliuncl  47072  sge0iunmptlemfi  47127  sge0rpcpnf  47135  iundjiun  47174  psmeasure  47185  ovnsubaddlem2  47285  hoidmvle  47314  ovolval4lem2  47364  smflimlem2  47486  smflimlem3  47487  smflimlem6  47490  smflimmpt  47524  fcoresf1  47806  icceuelpart  48185  gpgedgvtx0  48826  gpgedgvtx1  48827  srhmsubcALTV  49090  catprs  49789  thincciso2  50233  functermclem  50285  functermc  50286  fulltermc  50289