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 484	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 593	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  746  ad2ant2rl  749  cases2ALT  1048  consensus  1052  3ad2antr2  1188  3ad2antr3  1189  po2ne  5612  opabssxpd  5735  frpoind  6364  wfiOLD  6373  ordelord  6407  f1un  6868  f1cofveqaeqALT  7278  isocnv  7349  isores2  7352  f1oiso2  7371  offval  7705  ordsucun  7844  xp2nd  8045  2ndconst  8124  sexp2  8169  wfrdmclOLD  8355  smoord  8403  tfrlem9  8423  tfrlem11  8426  oaass  8597  omordi  8602  omwordri  8608  odi  8615  oewordri  8628  nnawordi  8657  nnmordi  8667  coflton  8707  dom2lem  9030  fundmen  9069  sbthlem9  9129  mapen  9179  mapunen  9184  ssenen  9189  domfi  9226  mapfien  9445  inf3lem6  9670  ttrclselem2  9763  frind  9787  r1val1  9823  rankval3b  9863  numacn  10086  infxpabs  10248  infxp  10251  cfsmolem  10307  infpssrlem4  10343  fin23lem27  10365  isf34lem4  10414  hsmexlem2  10464  axdc3lem2  10488  axdc3lem4  10490  iundom2g  10577  gchen1  10662  fpwwe2lem6  10673  fpwwe2lem10  10677  fpwwe2lem11  10678  prlem936  11084  muladd  11692  leord1  11787  eqord1  11788  ltord2  11789  leord2  11790  eqord2  11791  divadddiv  11979  ltmul12a  12120  lemul12b  12121  fimaxre  12209  supadd  12233  supmullem1  12235  cju  12259  zextlt  12689  zmax  12984  xrre  13207  supxr  13351  ixxdisj  13398  iooshf  13462  icodisj  13512  ioojoin  13519  iccshftr  13522  iccshftl  13524  iccdil  13526  icccntr  13528  iccf1o  13532  fzaddel  13594  fzsubel  13596  modadd1  13944  modmul1  13961  seqcaopr  14076  expsub  14147  expmordi  14203  sqlecan  14244  facndiv  14323  hashss  14444  hashfacen  14489  hashf1lem1  14490  fi1uzind  14542  brfi1indALT  14545  ccatpfx  14735  swrdccatfn  14758  swrdccatin2  14763  2cshwcshw  14860  resqrex  15285  fprodeq0  16007  lcmdvds  16641  hashdvds  16808  eulerthlem2  16815  pceu  16879  pcqcl  16889  infpnlem1  16943  4sqlem11  16988  ramcl  17062  prmgaplem5  17088  imasvscafn  17583  invfun  17811  initoeu2lem2  18068  catcisolem  18163  funcestrcsetclem8  18202  fullestrcsetc  18206  embedsetcestrclem  18212  funcsetcestrclem8  18217  fullsetcestrc  18221  prfcl  18258  prf1st  18259  prf2nd  18260  1st2ndprf  18261  curfuncf  18294  ipodrsfi  18596  mgmhmpropd  18723  subsubmgm  18735  mhmpropd  18817  subsubm  18841  pwsdiagmhm  18856  frmdgsum  18887  grplcan  19030  grplmulf1o  19043  grpraddf1o  19044  dfgrp3lem  19068  mulgsubcl  19118  subsubg  19179  eqger  19208  qus0subgadd  19229  resghm  19262  conjghm  19279  orbsta  19343  psgnunilem2  19527  odmulg  19588  sylow2a  19651  sylow3lem1  19659  lsmssv  19675  pj1ghm  19735  frgpup1  19807  ghmplusg  19878  subsubrng  20579  subsubrg  20614  srhmsubc  20696  issrngd  20872  lmhmco  21059  lmhmf1o  21062  lmhmima  21063  lmhmpreima  21064  reslmhm  21068  pwsdiaglmhm  21073  pwssplit2  21076  pwssplit3  21077  pj1lmhm  21116  lspdisj  21144  rngqiprngghmlem2  21315  rngqiprngghm  21326  prmirred  21502  cygznlem3  21605  frlmsslsp  21833  frlmlbs  21834  frlmup1  21835  issubassa2  21929  psrbagconf1o  21966  psrgrp  21993  evlslem2  22120  evlslem1  22123  ply1sclf1  22307  mamuass  22421  dmatmul  22518  dmatsubcl  22519  dmatmulcl  22521  dmatcrng  22523  scmatcrng  22542  mdetunilem9  22641  pm2mpghm  22837  fvmptnn04ifb  22872  toponmre  23116  neiptopreu  23156  ordtbas  23215  txcls  23627  txlm  23671  qtoptop2  23722  qtoprest  23740  kqt0lem  23759  ptuncnv  23830  fmfnfmlem4  23980  alexsubALTlem2  24071  tgpmulg  24116  blin  24446  xmeter  24458  xmetresbl  24462  dscmet  24600  nmdvr  24706  metnrmlem3  24896  icccvx  24994  bndth  25003  htpycc  25025  pcohtpylem  25065  pi1blem  25085  lmmbrf  25309  iscfil2  25313  iscau4  25326  minveclem7  25482  elovolm  25523  dyaddisjlem  25643  ismbfd  25687  itg1mulc  25753  dvlip  26046  dvcvx  26073  plypf1  26265  eff1olem  26604  logccv  26719  lawcos  26873  leibpilem1  26997  sqff1o  27239  dvdsppwf1o  27243  dvdsflf1o  27244  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  sgmmul  27259  fsumvma  27271  bposlem6  27347  lgsdchr  27413  rpvmasum2  27570  pntpbnd1  27644  ostthlem1  27685  sltres  27721  nodenselem5  27747  nodenselem6  27748  nodense  27751  addsproplem2  28017  mulsuniflem  28189  mulsunif2lem  28209  precsexlem9  28253  precsexlem10  28254  precsexlem11  28255  om2noseqlt2  28320  om2noseqf1o  28321  tgbtwntriv2  28509  ercgrg  28539  hlpasch  28778  colinearalglem4  28938  axlowdimlem15  28985  axcontlem7  28999  axcontlem8  29000  axcontlem10  29002  usgr1v  29287  pthdivtx  29761  clwwlkn1loopb  30071  grpolcan  30558  nvmf  30673  sspmval  30761  nmosetre  30792  minvecolem7  30911  hiassdi  31119  shscli  31345  fh1  31646  fh2  31647  cm2j  31648  chscllem2  31666  spansncvi  31680  5oalem2  31683  adjsym  31861  nmopsetretALT  31891  nmfnsetre  31905  cnvadj  31920  cnvunop  31946  unoplin  31948  hmoplin  31970  lnopmi  32028  hmops  32048  hmopm  32049  nmcexi  32054  adjlnop  32114  adjmul  32120  adjadd  32121  opsqrlem1  32168  mdsl0  32338  ssmd2  32340  mdexchi  32363  superpos  32382  chrelat2i  32393  atcvatlem  32413  atcvati  32414  chirredlem1  32418  chirredi  32422  atcvat3i  32424  atcvat4i  32425  mdsymlem3  32433  mdsymlem5  32435  cdj3lem2b  32465  ifnebib  32569  isoun  32716  xrge0infss  32770  1arithufdlem3  33553  extdg1id  33690  ddemeas  34216  fsum2dsub  34600  hgt750lemb  34649  bnj1145  34985  subfacp1lem3  35166  subfacp1lem5  35168  cvxpconn  35226  satfv1lem  35346  btwnconn1lem12  36079  colinbtwnle  36099  broutsideof2  36103  lineelsb2  36129  nn0prpwlem  36304  neibastop2lem  36342  tailfb  36359  onsuct0  36423  finxpreclem2  37372  lindsenlbs  37601  poimirlem4  37610  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  heicant  37641  mblfinlem2  37644  mblfinlem3  37645  ismblfin  37647  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anc  37687  sdclem1  37729  seqpo  37733  sstotbnd  37761  cntotbnd  37782  ismtycnv  37788  ismtyres  37794  heibor  37807  exidreslem  37863  ghomdiv  37878  grpokerinj  37879  rngohomco  37960  rngoisoco  37968  idlsubcl  38009  divrngidl  38014  ispridl2  38024  ispridlc  38056  riotasv3d  38941  omllaw3  39226  omlfh1N  39239  hlrelat2  39385  cvratlem  39403  cvrat  39404  cvrat3  39424  cvrat4  39425  ps-2  39460  elpaddn0  39782  paddss12  39801  pmodlem2  39829  cdleme0cq  40197  cdlemeg49lebilem  40521  cdleme50eq  40523  tendoeq2  40756  tendoex  40957  diameetN  41038  diainN  41039  dvhopN  41098  djajN  41119  dihmeetcl  41327  mapdheq2  41711  3factsumint1  42002  metakunt16  42201  imacrhmcl  42500  psrmnd  42531  evlsvvval  42549  evlselvlem  42572  fsuppind  42576  0prjspn  42614  fphpdo  42804  pell1234qrne0  42840  pell14qrgt0  42846  pell1qrge1  42857  monotoddzzfi  42930  jm2.18  42976  wepwsolem  43030  dnnumch3  43035  dnwech  43036  kelac1  43051  kercvrlsm  43071  onov0suclim  43263  cantnfresb  43313  dssmapnvod  44009  gsumws3  44185  gsumws4  44186  mnuprdlem1  44267  mnuprdlem2  44268  traxext  44937  cncmpmax  44969  fiiuncl  45004  choicefi  45142  fvelima2  45204  mullimc  45571  mullimcf  45578  idlimc  45581  limclner  45606  climleltrp  45631  limsupub  45659  climuzlem  45698  climliminflimsup2  45764  xlimbr  45782  xlimxrre  45786  dfxlim2v  45802  fperdvper  45874  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnprodlem1  45901  stoweidlem27  45982  stoweidlem48  46003  fourierdlem42  46104  fourierdlem63  46124  fourierdlem65  46126  dfsalgen2  46296  subsaliuncl  46313  sge0iunmptlemfi  46368  sge0rpcpnf  46376  iundjiun  46415  psmeasure  46426  ovnsubaddlem2  46526  hoidmvle  46555  ovolval4lem2  46605  smflimlem2  46727  smflimlem3  46728  smflimlem6  46731  smflimmpt  46765  fcoresf1  47018  icceuelpart  47360  gpgedgvtx0  47953  gpgedgvtx1  47954  srhmsubcALTV  48168  catprs  48799