Theorem adantrl 716

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  ad2ant2l  746  ad2ant2rl  749  cases2ALT  1049  consensus  1053  3ad2antr2  1191  3ad2antr3  1192  po2ne  5469  opabssxpd  5581  frpoind  6174  wfi  6181  ordelord  6213  f1cofveqaeqALT  7049  isocnv  7117  isores2  7120  f1oiso2  7139  offval  7455  ordsucun  7582  xp2nd  7772  2ndconst  7847  wfrdmcl  8041  smoord  8080  tfrlem9  8099  tfrlem11  8102  oaass  8267  omordi  8272  omwordri  8278  odi  8285  oewordri  8298  nnawordi  8327  nnmordi  8337  dom2lem  8646  fundmen  8686  sbthlem9  8742  mapen  8788  mapunen  8793  ssenen  8798  domfi  8874  mapfien  9002  inf3lem6  9226  r1val1  9367  rankval3b  9407  numacn  9628  infxpabs  9791  infxp  9794  cfsmolem  9849  infpssrlem4  9885  fin23lem27  9907  isf34lem4  9956  hsmexlem2  10006  axdc3lem2  10030  axdc3lem4  10032  iundom2g  10119  gchen1  10204  fpwwe2lem6  10215  fpwwe2lem10  10219  fpwwe2lem11  10220  prlem936  10626  muladd  11229  leord1  11324  eqord1  11325  ltord2  11326  leord2  11327  eqord2  11328  divadddiv  11512  ltmul12a  11653  lemul12b  11654  fimaxre  11741  supadd  11765  supmullem1  11767  cju  11791  zextlt  12216  zmax  12506  xrre  12724  supxr  12868  ixxdisj  12915  iooshf  12979  icodisj  13029  ioojoin  13036  iccshftr  13039  iccshftl  13041  iccdil  13043  icccntr  13045  iccf1o  13049  fzaddel  13111  fzsubel  13113  modadd1  13446  modmul1  13462  seqcaopr  13578  expsub  13648  expmordi  13702  sqlecan  13742  facndiv  13819  hashss  13941  hashfacen  13983  hashfacenOLD  13984  hashf1lem1  13985  hashf1lem1OLD  13986  fi1uzind  14028  brfi1indALT  14031  ccatpfx  14231  swrdccatfn  14254  swrdccatin2  14259  2cshwcshw  14355  resqrex  14779  fprodeq0  15500  lcmdvds  16128  hashdvds  16291  eulerthlem2  16298  pceu  16362  pcqcl  16372  infpnlem1  16426  4sqlem11  16471  ramcl  16545  prmgaplem5  16571  imasvscafn  16996  invfun  17223  initoeu2lem2  17475  catcisolem  17570  funcestrcsetclem8  17608  fullestrcsetc  17612  embedsetcestrclem  17618  funcsetcestrclem8  17623  fullsetcestrc  17627  prfcl  17664  prf1st  17665  prf2nd  17666  1st2ndprf  17667  curfuncf  17700  ipodrsfi  17999  mhmpropd  18178  subsubm  18197  pwsdiagmhm  18211  gsumccatOLD  18221  frmdgsum  18243  grplcan  18379  grplmulf1o  18391  dfgrp3lem  18415  mulgsubcl  18460  subsubg  18520  eqger  18548  resghm  18592  conjghm  18607  orbsta  18661  psgnunilem2  18841  odmulg  18901  sylow2a  18962  sylow3lem1  18970  lsmssv  18986  pj1ghm  19047  frgpup1  19119  ghmplusg  19185  subsubrg  19780  issrngd  19851  lmhmco  20034  lmhmf1o  20037  lmhmima  20038  lmhmpreima  20039  reslmhm  20043  pwsdiaglmhm  20048  pwssplit2  20051  pwssplit3  20052  pj1lmhm  20091  lspdisj  20116  prmirred  20415  cygznlem3  20488  frlmsslsp  20712  frlmlbs  20713  frlmup1  20714  issubassa2  20806  psrbagconf1o  20849  psrbagconf1oOLD  20850  evlslem2  20993  evlslem1  20996  ply1sclf1  21164  mamuass  21253  dmatmul  21348  dmatsubcl  21349  dmatmulcl  21351  dmatcrng  21353  scmatcrng  21372  mdetunilem9  21471  pm2mpghm  21667  fvmptnn04ifb  21702  toponmre  21944  neiptopreu  21984  ordtbas  22043  txcls  22455  txlm  22499  qtoptop2  22550  qtoprest  22568  kqt0lem  22587  ptuncnv  22658  fmfnfmlem4  22808  alexsubALTlem2  22899  tgpmulg  22944  blin  23273  xmeter  23285  xmetresbl  23289  dscmet  23424  nmdvr  23522  metnrmlem3  23712  icccvx  23801  bndth  23809  htpycc  23831  pcohtpylem  23870  pi1blem  23890  lmmbrf  24113  iscfil2  24117  iscau4  24130  minveclem7  24286  elovolm  24326  dyaddisjlem  24446  ismbfd  24490  itg1mulc  24556  dvlip  24844  dvcvx  24871  plypf1  25060  eff1olem  25391  logccv  25505  lawcos  25653  leibpilem1  25777  sqff1o  26018  dvdsppwf1o  26022  dvdsflf1o  26023  fsumdvdsmul  26031  sgmmul  26036  fsumvma  26048  bposlem6  26124  lgsdchr  26190  rpvmasum2  26347  pntpbnd1  26421  ostthlem1  26462  tgbtwntriv2  26532  ercgrg  26562  hlpasch  26801  colinearalglem4  26954  axlowdimlem15  27001  axcontlem7  27015  axcontlem8  27016  axcontlem10  27018  usgr1v  27298  pthdivtx  27770  clwwlkn1loopb  28080  grpolcan  28565  nvmf  28680  sspmval  28768  nmosetre  28799  minvecolem7  28918  hiassdi  29126  shscli  29352  fh1  29653  fh2  29654  cm2j  29655  chscllem2  29673  spansncvi  29687  5oalem2  29690  adjsym  29868  nmopsetretALT  29898  nmfnsetre  29912  cnvadj  29927  cnvunop  29953  unoplin  29955  hmoplin  29977  lnopmi  30035  hmops  30055  hmopm  30056  nmcexi  30061  adjlnop  30121  adjmul  30127  adjadd  30128  opsqrlem1  30175  mdsl0  30345  ssmd2  30347  mdexchi  30370  superpos  30389  chrelat2i  30400  atcvatlem  30420  atcvati  30421  chirredlem1  30425  chirredi  30429  atcvat3i  30431  atcvat4i  30432  mdsymlem3  30440  mdsymlem5  30442  cdj3lem2b  30472  isoun  30708  xrge0infss  30757  extdg1id  31406  ddemeas  31870  fsum2dsub  32253  hgt750lemb  32302  bnj1145  32640  subfacp1lem3  32811  subfacp1lem5  32813  satfv1lem  32991  frind  33460  sexp2  33473  sltres  33551  nodenselem5  33577  nodenselem6  33578  nodense  33581  btwnconn1lem12  34086  colinbtwnle  34106  broutsideof2  34110  lineelsb2  34136  nn0prpwlem  34197  neibastop2lem  34235  tailfb  34252  onsuct0  34316  finxpreclem2  35247  lindsenlbs  35458  poimirlem4  35467  poimirlem26  35489  poimirlem27  35490  poimirlem31  35494  heicant  35498  mblfinlem2  35501  mblfinlem3  35502  ismblfin  35504  ftc1anclem5  35540  ftc1anclem6  35541  ftc1anc  35544  sdclem1  35587  seqpo  35591  sstotbnd  35619  cntotbnd  35640  ismtycnv  35646  ismtyres  35652  heibor  35665  exidreslem  35721  ghomdiv  35736  grpokerinj  35737  rngohomco  35818  rngoisoco  35826  idlsubcl  35867  divrngidl  35872  ispridl2  35882  ispridlc  35914  riotasv3d  36660  omllaw3  36945  omlfh1N  36958  hlrelat2  37103  cvratlem  37121  cvrat  37122  cvrat3  37142  cvrat4  37143  ps-2  37178  elpaddn0  37500  paddss12  37519  pmodlem2  37547  cdleme0cq  37915  cdlemeg49lebilem  38239  cdleme50eq  38241  tendoeq2  38474  tendoex  38675  diameetN  38756  diainN  38757  dvhopN  38816  djajN  38837  dihmeetcl  39045  mapdheq2  39429  3factsumint1  39712  metakunt16  39803  evlsbagval  39926  fsuppind  39930  mhphf  39936  0prjspn  40114  fphpdo  40283  pell1234qrne0  40319  pell14qrgt0  40325  pell1qrge1  40336  monotoddzzfi  40408  jm2.18  40454  wepwsolem  40511  dnnumch3  40516  dnwech  40517  kelac1  40532  kercvrlsm  40552  dssmapnvod  41246  gsumws3  41426  gsumws4  41427  mnuprdlem1  41504  mnuprdlem2  41505  cncmpmax  42189  fiiuncl  42227  choicefi  42354  fvelima2  42419  mullimc  42775  mullimcf  42782  idlimc  42785  limclner  42810  climleltrp  42835  limsupub  42863  climuzlem  42902  climliminflimsup2  42968  xlimbr  42986  xlimxrre  42990  dfxlim2v  43006  fperdvper  43078  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvnprodlem1  43105  stoweidlem27  43186  stoweidlem48  43207  fourierdlem42  43308  fourierdlem63  43328  fourierdlem65  43330  dfsalgen2  43498  subsaliuncl  43515  sge0iunmptlemfi  43569  sge0rpcpnf  43577  iundjiun  43616  psmeasure  43627  ovnsubaddlem2  43727  hoidmvle  43756  ovolval4lem2  43806  ovolval5lem3  43810  smflimlem2  43922  smflimlem3  43923  smflimlem6  43926  smflimmpt  43958  fcoresf1  44178  icceuelpart  44504  mgmhmpropd  44955  subsubmgm  44967  srhmsubc  45250  srhmsubcALTV  45268  catprs  45908