Theorem adantrl 726

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 602	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 209  df-an 400

This theorem is referenced by:  ad2ant2l  756  ad2ant2rl  759  cases2ALT  1059  consensus  1063  3ad2antr2  1202  3ad2antr3  1203  po2ne  5567  opabssxpd  5690  frpoind  6324  ordelord  6363  f1un  6822  fvelima2  6914  f1cofveqaeqALT  7237  isocnv  7309  isores2  7312  f1oiso2  7331  offval  7664  ordsucun  7800  xp2nd  7998  2ndconst  8074  sexp2  8120  smoord  8330  tfrlem9  8350  tfrlem11  8353  oaass  8524  omordi  8529  omwordri  8535  odi  8542  oewordri  8556  nnawordi  8585  nnmordi  8595  coflton  8635  dom2lem  8967  fundmen  9006  sbthlem9  9061  mapen  9107  mapunen  9112  ssenen  9117  domfi  9151  mapfien  9348  inf3lem6  9582  ttrclselem2  9675  frind  9702  r1val1  9738  rankval3b  9778  numacn  9999  infxpabs  10161  infxp  10164  cfsmolem  10221  infpssrlem4  10257  fin23lem27  10279  isf34lem4  10328  hsmexlem2  10378  axdc3lem2  10402  axdc3lem4  10404  iundom2g  10491  gchen1  10577  fpwwe2lem6  10588  fpwwe2lem10  10592  fpwwe2lem11  10593  prlem936  10999  muladd  11613  leord1  11708  eqord1  11709  ltord2  11710  leord2  11711  eqord2  11712  divadddiv  11900  ltmul12a  12041  lemul12b  12042  fimaxre  12130  supadd  12154  supmullem1  12156  cju  12185  zextlt  12641  zmax  12940  xrre  13166  supxr  13310  ixxdisj  13358  iooshf  13424  icodisj  13474  ioojoin  13481  iccshftr  13484  iccshftl  13486  iccdil  13488  icccntr  13490  iccf1o  13494  fzaddel  13557  fzsubel  13559  modadd1  13912  modmul1  13931  seqcaopr  14046  expsub  14117  expmordi  14174  sqlecan  14216  facndiv  14295  hashss  14416  hashfacen  14461  hashf1lem1  14462  fi1uzind  14514  brfi1indALT  14517  ccatpfx  14708  swrdccatfn  14731  swrdccatin2  14736  2cshwcshw  14832  resqrex  15268  fprodeq0  15996  lcmdvds  16633  hashdvds  16801  eulerthlem2  16808  pceu  16873  pcqcl  16883  infpnlem1  16937  4sqlem11  16982  ramcl  17056  prmgaplem5  17082  imasvscafn  17558  invfun  17788  initoeu2lem2  18039  catcisolem  18134  funcestrcsetclem8  18170  fullestrcsetc  18174  embedsetcestrclem  18180  funcsetcestrclem8  18185  fullsetcestrc  18189  prfcl  18226  prf1st  18227  prf2nd  18228  1st2ndprf  18229  curfuncf  18261  ipodrsfi  18562  mgmhmpropd  18723  subsubmgm  18735  mhmpropd  18817  subsubm  18841  pwsdiagmhm  18856  frmdgsum  18887  grplcan  19033  grplmulf1o  19046  grpraddf1o  19047  dfgrp3lem  19071  mulgsubcl  19121  subsubg  19182  eqger  19210  qus0subgadd  19231  resghm  19263  conjghm  19280  orbsta  19344  psgnunilem2  19526  odmulg  19587  sylow2a  19650  sylow3lem1  19658  lsmssv  19674  pj1ghm  19734  frgpup1  19806  ghmplusg  19877  subsubrng  20600  subsubrg  20635  srhmsubc  20717  issrngd  20892  lmhmco  21098  lmhmf1o  21101  lmhmima  21102  lmhmpreima  21103  reslmhm  21107  pwsdiaglmhm  21112  pwssplit2  21115  pwssplit3  21116  pj1lmhm  21155  lspdisj  21183  rngqiprngghmlem2  21346  rngqiprngghm  21357  prmirred  21514  cygznlem3  21609  frlmsslsp  21836  frlmlbs  21837  frlmup1  21838  issubassa2  21932  psrbagconf1o  21969  psrgrp  21996  evlslem2  22120  evlslem1  22123  evlsvvval  22134  ply1sclf1  22340  mamuass  22450  dmatmul  22545  dmatsubcl  22546  dmatmulcl  22548  dmatcrng  22550  scmatcrng  22569  mdetunilem9  22668  pm2mpghm  22864  fvmptnn04ifb  22899  toponmre  23141  neiptopreu  23181  ordtbas  23240  txcls  23652  txlm  23696  qtoptop2  23747  qtoprest  23765  kqt0lem  23784  ptuncnv  23855  fmfnfmlem4  24005  alexsubALTlem2  24096  tgpmulg  24141  blin  24469  xmeter  24481  xmetresbl  24485  dscmet  24620  nmdvr  24718  metnrmlem3  24910  icccvx  25000  bndth  25008  htpycc  25030  pcohtpylem  25069  pi1blem  25089  lmmbrf  25312  iscfil2  25316  iscau4  25329  minveclem7  25485  elovolm  25525  dyaddisjlem  25645  ismbfd  25689  itg1mulc  25754  dvlip  26043  dvcvx  26070  plypf1  26260  eff1olem  26601  logccv  26716  lawcos  26869  leibpilem1  26993  sqff1o  27234  dvdsppwf1o  27238  dvdsflf1o  27239  fsumdvdsmul  27247  sgmmul  27253  fsumvma  27265  bposlem6  27341  lgsdchr  27407  rpvmasum2  27564  pntpbnd1  27638  ostthlem1  27679  ltsres  27714  nodenselem5  27740  nodenselem6  27741  nodense  27744  addsproplem2  28051  mulsuniflem  28230  mulsunif2lem  28250  precsexlem9  28296  precsexlem10  28297  precsexlem11  28298  om2noseqlt2  28381  om2noseqf1o  28382  z12sge0  28564  elreno2  28576  tgbtwntriv2  28644  ercgrg  28674  hlpasch  28913  colinearalglem4  29067  axlowdimlem15  29114  axcontlem7  29128  axcontlem8  29129  axcontlem10  29131  usgr1v  29414  pthdivtx  29884  clwwlkn1loopb  30202  grpolcan  30690  nvmf  30805  sspmval  30893  nmosetre  30924  minvecolem7  31043  hiassdi  31251  shscli  31477  fh1  31778  fh2  31779  cm2j  31780  chscllem2  31798  spansncvi  31812  5oalem2  31815  adjsym  31993  nmopsetretALT  32023  nmfnsetre  32037  cnvadj  32052  cnvunop  32078  unoplin  32080  hmoplin  32102  lnopmi  32160  hmops  32180  hmopm  32181  nmcexi  32186  adjlnop  32246  adjmul  32252  adjadd  32253  opsqrlem1  32300  mdsl0  32470  ssmd2  32472  mdexchi  32495  superpos  32514  chrelat2i  32525  atcvatlem  32545  atcvati  32546  chirredlem1  32550  chirredi  32554  atcvat3i  32556  atcvat4i  32557  mdsymlem3  32565  mdsymlem5  32567  cdj3lem2b  32597  ifnebib  32708  isoun  32865  xrge0infss  32923  1arithufdlem3  33703  extdg1id  33924  ddemeas  34494  fsum2dsub  34862  hgt750lemb  34911  bnj1145  35249  subfacp1lem3  35493  subfacp1lem5  35495  cvxpconn  35553  satfv1lem  35673  btwnconn1lem12  36409  colinbtwnle  36429  broutsideof2  36433  lineelsb2  36459  nn0prpwlem  36643  neibastop2lem  36681  tailfb  36698  onsuct0  36762  finxpreclem2  37845  lindsenlbs  38075  poimirlem4  38084  poimirlem26  38106  poimirlem27  38107  poimirlem31  38111  heicant  38115  mblfinlem2  38118  mblfinlem3  38119  ismblfin  38121  ftc1anclem5  38157  ftc1anclem6  38158  ftc1anc  38161  sdclem1  38203  seqpo  38207  sstotbnd  38235  cntotbnd  38256  ismtycnv  38262  ismtyres  38268  heibor  38281  exidreslem  38337  ghomdiv  38352  grpokerinj  38353  rngohomco  38434  rngoisoco  38442  idlsubcl  38483  divrngidl  38488  ispridl2  38498  ispridlc  38530  riotasv3d  39545  omllaw3  39830  omlfh1N  39843  hlrelat2  39988  cvratlem  40006  cvrat  40007  cvrat3  40027  cvrat4  40028  ps-2  40063  elpaddn0  40385  paddss12  40404  pmodlem2  40432  cdleme0cq  40800  cdlemeg49lebilem  41124  cdleme50eq  41126  tendoeq2  41359  tendoex  41560  diameetN  41641  diainN  41642  dvhopN  41701  djajN  41722  dihmeetcl  41930  mapdheq2  42314  3factsumint1  42599  imacrhmcl  43097  psrmnd  43122  evlselvlem  43131  fsuppind  43133  0prjspn  43171  fphpdo  43355  pell1234qrne0  43391  pell14qrgt0  43397  pell1qrge1  43408  monotoddzzfi  43480  jm2.18  43526  wepwsolem  43580  dnnumch3  43585  dnwech  43586  kelac1  43601  kercvrlsm  43621  onov0suclim  43812  cantnfresb  43862  dssmapnvod  44557  gsumws3  44733  gsumws4  44734  mnuprdlem1  44809  mnuprdlem2  44810  traxext  45514  modelac8prim  45529  cncmpmax  45573  fiiuncl  45606  choicefi  45738  mullimc  46153  mullimcf  46160  idlimc  46163  limclner  46186  climleltrp  46211  limsupub  46239  climuzlem  46278  climliminflimsup2  46344  xlimbr  46362  xlimxrre  46366  dfxlim2v  46382  fperdvper  46454  ioodvbdlimc1lem2  46467  ioodvbdlimc2lem  46469  dvnprodlem1  46481  stoweidlem27  46562  stoweidlem48  46583  fourierdlem42  46684  fourierdlem63  46704  fourierdlem65  46706  dfsalgen2  46876  subsaliuncl  46893  sge0iunmptlemfi  46948  sge0rpcpnf  46956  iundjiun  46995  psmeasure  47006  ovnsubaddlem2  47106  hoidmvle  47135  ovolval4lem2  47185  smflimlem2  47307  smflimlem3  47308  smflimlem6  47311  smflimmpt  47345  fcoresf1  47624  icceuelpart  48003  gpgedgvtx0  48644  gpgedgvtx1  48645  srhmsubcALTV  48908  catprs  49593  thincciso2  50037  functermclem  50089  functermc  50090  fulltermc  50093