Theorem adantrl 715

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad2ant2l  745  ad2ant2rl  748  cases2ALT  1049  consensus  1053  3ad2antr2  1189  3ad2antr3  1190  po2ne  5624  opabssxpd  5747  frpoind  6374  wfiOLD  6383  ordelord  6417  f1un  6882  f1cofveqaeqALT  7296  isocnv  7366  isores2  7369  f1oiso2  7388  offval  7723  ordsucun  7861  xp2nd  8063  2ndconst  8142  sexp2  8187  wfrdmclOLD  8373  smoord  8421  tfrlem9  8441  tfrlem11  8444  oaass  8617  omordi  8622  omwordri  8628  odi  8635  oewordri  8648  nnawordi  8677  nnmordi  8687  coflton  8727  dom2lem  9052  fundmen  9096  sbthlem9  9157  mapen  9207  mapunen  9212  ssenen  9217  domfi  9255  mapfien  9477  inf3lem6  9702  ttrclselem2  9795  frind  9819  r1val1  9855  rankval3b  9895  numacn  10118  infxpabs  10280  infxp  10283  cfsmolem  10339  infpssrlem4  10375  fin23lem27  10397  isf34lem4  10446  hsmexlem2  10496  axdc3lem2  10520  axdc3lem4  10522  iundom2g  10609  gchen1  10694  fpwwe2lem6  10705  fpwwe2lem10  10709  fpwwe2lem11  10710  prlem936  11116  muladd  11722  leord1  11817  eqord1  11818  ltord2  11819  leord2  11820  eqord2  11821  divadddiv  12009  ltmul12a  12150  lemul12b  12151  fimaxre  12239  supadd  12263  supmullem1  12265  cju  12289  zextlt  12717  zmax  13010  xrre  13231  supxr  13375  ixxdisj  13422  iooshf  13486  icodisj  13536  ioojoin  13543  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  iccf1o  13556  fzaddel  13618  fzsubel  13620  modadd1  13959  modmul1  13975  seqcaopr  14090  expsub  14161  expmordi  14217  sqlecan  14258  facndiv  14337  hashss  14458  hashfacen  14503  hashf1lem1  14504  fi1uzind  14556  brfi1indALT  14559  ccatpfx  14749  swrdccatfn  14772  swrdccatin2  14777  2cshwcshw  14874  resqrex  15299  fprodeq0  16023  lcmdvds  16655  hashdvds  16822  eulerthlem2  16829  pceu  16893  pcqcl  16903  infpnlem1  16957  4sqlem11  17002  ramcl  17076  prmgaplem5  17102  imasvscafn  17597  invfun  17825  initoeu2lem2  18082  catcisolem  18177  funcestrcsetclem8  18216  fullestrcsetc  18220  embedsetcestrclem  18226  funcsetcestrclem8  18231  fullsetcestrc  18235  prfcl  18272  prf1st  18273  prf2nd  18274  1st2ndprf  18275  curfuncf  18308  ipodrsfi  18609  mgmhmpropd  18736  subsubmgm  18748  mhmpropd  18827  subsubm  18851  pwsdiagmhm  18866  frmdgsum  18897  grplcan  19040  grplmulf1o  19053  grpraddf1o  19054  dfgrp3lem  19078  mulgsubcl  19128  subsubg  19189  eqger  19218  qus0subgadd  19239  resghm  19272  conjghm  19289  orbsta  19353  psgnunilem2  19537  odmulg  19598  sylow2a  19661  sylow3lem1  19669  lsmssv  19685  pj1ghm  19745  frgpup1  19817  ghmplusg  19888  subsubrng  20589  subsubrg  20626  srhmsubc  20702  issrngd  20878  lmhmco  21065  lmhmf1o  21068  lmhmima  21069  lmhmpreima  21070  reslmhm  21074  pwsdiaglmhm  21079  pwssplit2  21082  pwssplit3  21083  pj1lmhm  21122  lspdisj  21150  rngqiprngghmlem2  21321  rngqiprngghm  21332  prmirred  21508  cygznlem3  21611  frlmsslsp  21839  frlmlbs  21840  frlmup1  21841  issubassa2  21935  psrbagconf1o  21972  psrgrp  21999  evlslem2  22126  evlslem1  22129  ply1sclf1  22313  mamuass  22427  dmatmul  22524  dmatsubcl  22525  dmatmulcl  22527  dmatcrng  22529  scmatcrng  22548  mdetunilem9  22647  pm2mpghm  22843  fvmptnn04ifb  22878  toponmre  23122  neiptopreu  23162  ordtbas  23221  txcls  23633  txlm  23677  qtoptop2  23728  qtoprest  23746  kqt0lem  23765  ptuncnv  23836  fmfnfmlem4  23986  alexsubALTlem2  24077  tgpmulg  24122  blin  24452  xmeter  24464  xmetresbl  24468  dscmet  24606  nmdvr  24712  metnrmlem3  24902  icccvx  25000  bndth  25009  htpycc  25031  pcohtpylem  25071  pi1blem  25091  lmmbrf  25315  iscfil2  25319  iscau4  25332  minveclem7  25488  elovolm  25529  dyaddisjlem  25649  ismbfd  25693  itg1mulc  25759  dvlip  26052  dvcvx  26079  plypf1  26271  eff1olem  26608  logccv  26723  lawcos  26877  leibpilem1  27001  sqff1o  27243  dvdsppwf1o  27247  dvdsflf1o  27248  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  sgmmul  27263  fsumvma  27275  bposlem6  27351  lgsdchr  27417  rpvmasum2  27574  pntpbnd1  27648  ostthlem1  27689  sltres  27725  nodenselem5  27751  nodenselem6  27752  nodense  27755  addsproplem2  28021  mulsuniflem  28193  mulsunif2lem  28213  precsexlem9  28257  precsexlem10  28258  precsexlem11  28259  om2noseqlt2  28324  om2noseqf1o  28325  tgbtwntriv2  28513  ercgrg  28543  hlpasch  28782  colinearalglem4  28942  axlowdimlem15  28989  axcontlem7  29003  axcontlem8  29004  axcontlem10  29006  usgr1v  29291  pthdivtx  29765  clwwlkn1loopb  30075  grpolcan  30562  nvmf  30677  sspmval  30765  nmosetre  30796  minvecolem7  30915  hiassdi  31123  shscli  31349  fh1  31650  fh2  31651  cm2j  31652  chscllem2  31670  spansncvi  31684  5oalem2  31687  adjsym  31865  nmopsetretALT  31895  nmfnsetre  31909  cnvadj  31924  cnvunop  31950  unoplin  31952  hmoplin  31974  lnopmi  32032  hmops  32052  hmopm  32053  nmcexi  32058  adjlnop  32118  adjmul  32124  adjadd  32125  opsqrlem1  32172  mdsl0  32342  ssmd2  32344  mdexchi  32367  superpos  32386  chrelat2i  32397  atcvatlem  32417  atcvati  32418  chirredlem1  32422  chirredi  32426  atcvat3i  32428  atcvat4i  32429  mdsymlem3  32437  mdsymlem5  32439  cdj3lem2b  32469  ifnebib  32572  isoun  32713  xrge0infss  32767  1arithufdlem3  33539  extdg1id  33676  ddemeas  34200  fsum2dsub  34584  hgt750lemb  34633  bnj1145  34969  subfacp1lem3  35150  subfacp1lem5  35152  cvxpconn  35210  satfv1lem  35330  btwnconn1lem12  36062  colinbtwnle  36082  broutsideof2  36086  lineelsb2  36112  nn0prpwlem  36288  neibastop2lem  36326  tailfb  36343  onsuct0  36407  finxpreclem2  37356  lindsenlbs  37575  poimirlem4  37584  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  heicant  37615  mblfinlem2  37618  mblfinlem3  37619  ismblfin  37621  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anc  37661  sdclem1  37703  seqpo  37707  sstotbnd  37735  cntotbnd  37756  ismtycnv  37762  ismtyres  37768  heibor  37781  exidreslem  37837  ghomdiv  37852  grpokerinj  37853  rngohomco  37934  rngoisoco  37942  idlsubcl  37983  divrngidl  37988  ispridl2  37998  ispridlc  38030  riotasv3d  38916  omllaw3  39201  omlfh1N  39214  hlrelat2  39360  cvratlem  39378  cvrat  39379  cvrat3  39399  cvrat4  39400  ps-2  39435  elpaddn0  39757  paddss12  39776  pmodlem2  39804  cdleme0cq  40172  cdlemeg49lebilem  40496  cdleme50eq  40498  tendoeq2  40731  tendoex  40932  diameetN  41013  diainN  41014  dvhopN  41073  djajN  41094  dihmeetcl  41302  mapdheq2  41686  3factsumint1  41978  metakunt16  42177  imacrhmcl  42469  psrmnd  42500  evlsvvval  42518  evlselvlem  42541  fsuppind  42545  0prjspn  42583  fphpdo  42773  pell1234qrne0  42809  pell14qrgt0  42815  pell1qrge1  42826  monotoddzzfi  42899  jm2.18  42945  wepwsolem  42999  dnnumch3  43004  dnwech  43005  kelac1  43020  kercvrlsm  43040  onov0suclim  43236  cantnfresb  43286  dssmapnvod  43982  gsumws3  44158  gsumws4  44159  mnuprdlem1  44241  mnuprdlem2  44242  traxext  44910  cncmpmax  44932  fiiuncl  44967  choicefi  45107  fvelima2  45169  mullimc  45537  mullimcf  45544  idlimc  45547  limclner  45572  climleltrp  45597  limsupub  45625  climuzlem  45664  climliminflimsup2  45730  xlimbr  45748  xlimxrre  45752  dfxlim2v  45768  fperdvper  45840  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnprodlem1  45867  stoweidlem27  45948  stoweidlem48  45969  fourierdlem42  46070  fourierdlem63  46090  fourierdlem65  46092  dfsalgen2  46262  subsaliuncl  46279  sge0iunmptlemfi  46334  sge0rpcpnf  46342  iundjiun  46381  psmeasure  46392  ovnsubaddlem2  46492  hoidmvle  46521  ovolval4lem2  46571  smflimlem2  46693  smflimlem3  46694  smflimlem6  46697  smflimmpt  46731  fcoresf1  46984  icceuelpart  47310  srhmsubcALTV  48048  catprs  48678