Theorem adantrl 714

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  ad2ant2l  744  ad2ant2rl  747  cases2ALT  1043  consensus  1047  3ad2antr2  1185  3ad2antr3  1186  po2ne  5489  opabssxpd  5789  wfi  6181  ordelord  6213  foco  6602  f1cofveqaeqALT  7017  isocnv  7083  isores2  7086  f1oiso2  7105  offval  7416  ordsucun  7540  xp2nd  7722  2ndconst  7796  wfrdmcl  7963  smoord  8002  tfrlem9  8021  tfrlem11  8024  oaass  8187  omordi  8192  omwordri  8198  odi  8205  oewordri  8218  nnawordi  8247  nnmordi  8257  dom2lem  8549  fundmen  8583  sbthlem9  8635  mapen  8681  mapunen  8686  ssenen  8691  domfi  8739  mapfien  8871  inf3lem6  9096  r1val1  9215  rankval3b  9255  numacn  9475  infxpabs  9634  infxp  9637  cfsmolem  9692  infpssrlem4  9728  fin23lem27  9750  isf34lem4  9799  hsmexlem2  9849  axdc3lem2  9873  axdc3lem4  9875  iundom2g  9962  gchen1  10047  fpwwe2lem7  10058  fpwwe2lem11  10062  fpwwe2lem12  10063  prlem936  10469  muladd  11072  leord1  11167  eqord1  11168  ltord2  11169  leord2  11170  eqord2  11171  divadddiv  11355  ltmul12a  11496  lemul12b  11497  fimaxre  11584  supadd  11609  supmullem1  11611  cju  11634  zextlt  12057  zmax  12346  xrre  12563  supxr  12707  ixxdisj  12754  iooshf  12816  icodisj  12863  ioojoin  12870  iccshftr  12873  iccshftl  12875  iccdil  12877  icccntr  12879  iccf1o  12883  fzaddel  12942  fzsubel  12944  modadd1  13277  modmul1  13293  seqcaopr  13408  expsub  13478  expmordi  13532  sqlecan  13572  facndiv  13649  hashss  13771  hashfacen  13813  hashf1lem1  13814  fi1uzind  13856  brfi1indALT  13859  ccatpfx  14063  swrdccatfn  14086  swrdccatin2  14091  2cshwcshw  14187  resqrex  14610  fprodeq0  15329  lcmdvds  15952  hashdvds  16112  eulerthlem2  16119  pceu  16183  pcqcl  16193  infpnlem1  16246  4sqlem11  16291  ramcl  16365  prmgaplem5  16391  imasvscafn  16810  invfun  17034  initoeu2lem2  17275  catcisolem  17366  funcestrcsetclem8  17397  fullestrcsetc  17401  embedsetcestrclem  17407  funcsetcestrclem8  17412  fullsetcestrc  17416  prfcl  17453  prf1st  17454  prf2nd  17455  1st2ndprf  17456  curfuncf  17488  ipodrsfi  17773  mhmpropd  17962  subsubm  17981  pwsdiagmhm  17995  gsumccatOLD  18005  frmdgsum  18027  grplcan  18161  grplmulf1o  18173  dfgrp3lem  18197  mulgsubcl  18242  subsubg  18302  eqger  18330  resghm  18374  conjghm  18389  orbsta  18443  psgnunilem2  18623  odmulg  18683  sylow2a  18744  sylow3lem1  18752  lsmssv  18768  pj1ghm  18829  frgpup1  18901  ghmplusg  18966  subsubrg  19561  issrngd  19632  lmhmco  19815  lmhmf1o  19818  lmhmima  19819  lmhmpreima  19820  reslmhm  19824  pwsdiaglmhm  19829  pwssplit2  19832  pwssplit3  19833  pj1lmhm  19872  lspdisj  19897  issubassa2  20121  psrbagconf1o  20154  evlslem2  20292  evlslem1  20295  ply1sclf1  20457  prmirred  20642  cygznlem3  20716  frlmsslsp  20940  frlmlbs  20941  frlmup1  20942  mamuass  21011  dmatmul  21106  dmatsubcl  21107  dmatmulcl  21109  dmatcrng  21111  scmatcrng  21130  mdetunilem9  21229  pm2mpghm  21424  fvmptnn04ifb  21459  toponmre  21701  neiptopreu  21741  ordtbas  21800  txcls  22212  txlm  22256  qtoptop2  22307  qtoprest  22325  kqt0lem  22344  ptuncnv  22415  fmfnfmlem4  22565  alexsubALTlem2  22656  tgpmulg  22701  blin  23031  xmeter  23043  xmetresbl  23047  dscmet  23182  nmdvr  23279  metnrmlem3  23469  icccvx  23554  bndth  23562  htpycc  23584  pcohtpylem  23623  pi1blem  23643  lmmbrf  23865  iscfil2  23869  iscau4  23882  minveclem7  24038  elovolm  24076  dyaddisjlem  24196  ismbfd  24240  itg1mulc  24305  dvlip  24590  dvcvx  24617  plypf1  24802  eff1olem  25132  logccv  25246  lawcos  25394  leibpilem1  25518  sqff1o  25759  dvdsppwf1o  25763  dvdsflf1o  25764  fsumdvdsmul  25772  sgmmul  25777  fsumvma  25789  bposlem6  25865  lgsdchr  25931  rpvmasum2  26088  pntpbnd1  26162  ostthlem1  26203  tgbtwntriv2  26273  ercgrg  26303  hlpasch  26542  colinearalglem4  26695  axlowdimlem15  26742  axcontlem7  26756  axcontlem8  26757  axcontlem10  26759  usgr1v  27038  pthdivtx  27510  clwwlkn1loopb  27821  grpolcan  28307  nvmf  28422  sspmval  28510  nmosetre  28541  minvecolem7  28660  hiassdi  28868  shscli  29094  fh1  29395  fh2  29396  cm2j  29397  chscllem2  29415  spansncvi  29429  5oalem2  29432  adjsym  29610  nmopsetretALT  29640  nmfnsetre  29654  cnvadj  29669  cnvunop  29695  unoplin  29697  hmoplin  29719  lnopmi  29777  hmops  29797  hmopm  29798  nmcexi  29803  adjlnop  29863  adjmul  29869  adjadd  29870  opsqrlem1  29917  mdsl0  30087  ssmd2  30089  mdexchi  30112  superpos  30131  chrelat2i  30142  atcvatlem  30162  atcvati  30163  chirredlem1  30167  chirredi  30171  atcvat3i  30173  atcvat4i  30174  mdsymlem3  30182  mdsymlem5  30184  cdj3lem2b  30214  isoun  30437  xrge0infss  30484  extdg1id  31053  ddemeas  31495  fsum2dsub  31878  hgt750lemb  31927  bnj1145  32265  subfacp1lem3  32429  subfacp1lem5  32431  satfv1lem  32609  frpoind  33080  frind  33085  sltres  33169  nodenselem5  33192  nodenselem6  33193  nodense  33196  btwnconn1lem12  33559  colinbtwnle  33579  broutsideof2  33583  lineelsb2  33609  nn0prpwlem  33670  neibastop2lem  33708  tailfb  33725  onsuct0  33789  finxpreclem2  34674  lindsenlbs  34902  poimirlem4  34911  poimirlem26  34933  poimirlem27  34934  poimirlem31  34938  heicant  34942  mblfinlem2  34945  mblfinlem3  34946  ismblfin  34948  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anc  34990  sdclem1  35033  seqpo  35037  sstotbnd  35068  cntotbnd  35089  ismtycnv  35095  ismtyres  35101  heibor  35114  exidreslem  35170  ghomdiv  35185  grpokerinj  35186  rngohomco  35267  rngoisoco  35275  idlsubcl  35316  divrngidl  35321  ispridl2  35331  ispridlc  35363  riotasv3d  36111  omllaw3  36396  omlfh1N  36409  hlrelat2  36554  cvratlem  36572  cvrat  36573  cvrat3  36593  cvrat4  36594  ps-2  36629  elpaddn0  36951  paddss12  36970  pmodlem2  36998  cdleme0cq  37366  cdlemeg49lebilem  37690  cdleme50eq  37692  tendoeq2  37925  tendoex  38126  diameetN  38207  diainN  38208  dvhopN  38267  djajN  38288  dihmeetcl  38496  mapdheq2  38880  0prjspn  39290  fphpdo  39434  pell1234qrne0  39470  pell14qrgt0  39476  pell1qrge1  39487  monotoddzzfi  39559  jm2.18  39605  wepwsolem  39662  dnnumch3  39667  dnwech  39668  kelac1  39683  kercvrlsm  39703  dssmapnvod  40386  gsumws3  40569  gsumws4  40570  mnuprdlem1  40628  mnuprdlem2  40629  cncmpmax  41309  fiiuncl  41347  choicefi  41483  fvelima2  41552  mullimc  41917  mullimcf  41924  idlimc  41927  limclner  41952  climleltrp  41977  limsupub  42005  climuzlem  42044  climliminflimsup2  42110  xlimbr  42128  xlimxrre  42132  dfxlim2v  42148  fperdvper  42223  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvnprodlem1  42251  stoweidlem27  42332  stoweidlem48  42353  fourierdlem42  42454  fourierdlem63  42474  fourierdlem65  42476  dfsalgen2  42644  subsaliuncl  42661  sge0iunmptlemfi  42715  sge0rpcpnf  42723  iundjiun  42762  psmeasure  42773  ovnsubaddlem2  42873  hoidmvle  42902  ovolval4lem2  42952  ovolval5lem3  42956  smflimlem2  43068  smflimlem3  43069  smflimlem6  43072  smflimmpt  43104  icceuelpart  43616  mgmhmpropd  44072  subsubmgm  44084  srhmsubc  44367  srhmsubcALTV  44385