Theorem adantrl 752

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  ad2ant2l  782  ad2ant2rl  785  cases2  993  consensus  999  3ad2antr2  1227  3ad2antr3  1228  opabssxpd  5338  wfi  5713  ordelord  5745  foco  6125  f1cofveqaeqALT  6516  isocnv  6580  isores2  6583  f1oiso2  6602  offval  6904  ordsucun  7025  xp2nd  7199  1stconst  7265  2ndconst  7266  wfrdmcl  7423  smoord  7462  tfrlem9  7481  tfrlem11  7484  oaass  7641  omordi  7646  omwordri  7652  odi  7659  oewordri  7672  nnawordi  7701  nnmordi  7711  dom2lem  7995  fundmen  8030  sbthlem9  8078  mapen  8124  mapunen  8129  ssenen  8134  domfi  8181  mapfien  8313  inf3lem6  8530  r1val1  8649  rankval3b  8689  numacn  8872  infxpabs  9034  infxp  9037  cfsmolem  9092  infpssrlem4  9128  fin23lem27  9150  isf34lem4  9199  hsmexlem2  9249  axdc3lem2  9273  axdc3lem4  9275  iundom2g  9362  gchen1  9447  fpwwe2lem7  9458  fpwwe2lem11  9462  fpwwe2lem12  9463  prlem936  9869  muladd  10462  leord1  10555  eqord1  10556  ltord2  10557  leord2  10558  eqord2  10559  divadddiv  10740  ltmul12a  10879  lemul12b  10880  supadd  10991  supmullem1  10993  cju  11016  zextlt  11451  zmax  11785  xrre  12000  supxr  12143  ixxdisj  12190  iooshf  12252  icodisj  12297  ioojoin  12303  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  iccf1o  12316  fzaddel  12375  fzsubel  12377  modadd1  12707  modmul1  12723  seqcaopr  12838  expsub  12908  sqlecan  12971  facndiv  13075  hashss  13197  hashfacen  13238  hashf1lem1  13239  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  swrdccatin12lem2b  13486  2cshwcshw  13571  resqrex  13991  fprodeq0  14705  lcmdvds  15321  hashdvds  15480  eulerthlem2  15487  pceu  15551  pcqcl  15561  infpnlem1  15614  4sqlem11  15659  ramcl  15733  prmgaplem5  15759  imasvscafn  16197  invfun  16424  initoeu2lem2  16665  catcisolem  16756  funcestrcsetclem8  16787  fullestrcsetc  16791  embedsetcestrclem  16797  funcsetcestrclem8  16802  fullsetcestrc  16806  prfcl  16843  prf1st  16844  prf2nd  16845  1st2ndprf  16846  curfuncf  16878  ipodrsfi  17163  mhmpropd  17341  subsubm  17357  pwsdiagmhm  17369  gsumccat  17378  frmdgsum  17399  grplcan  17477  grplmulf1o  17489  dfgrp3lem  17513  mulgsubcl  17555  subsubg  17617  eqger  17644  resghm  17676  conjghm  17691  orbsta  17746  psgnunilem2  17915  odmulg  17973  sylow2a  18034  sylow3lem1  18042  lsmssv  18058  pj1ghm  18116  frgpup1  18188  ghmplusg  18249  subsubrg  18806  issrngd  18861  lmhmco  19043  lmhmf1o  19046  lmhmima  19047  lmhmpreima  19048  reslmhm  19052  pwsdiaglmhm  19057  pwssplit2  19060  pwssplit3  19061  pj1lmhm  19100  lspdisj  19125  issubassa2  19345  psrbagconf1o  19374  evlslem2  19512  evlslem1  19515  ply1sclf1  19659  prmirred  19843  cygznlem3  19918  frlmsslsp  20135  frlmlbs  20136  frlmup1  20137  mamuass  20208  dmatmul  20303  dmatsubcl  20304  dmatmulcl  20306  dmatcrng  20308  scmatcrng  20327  mdetunilem9  20426  pm2mpghm  20621  fvmptnn04ifb  20656  toponmre  20897  neiptopreu  20937  ordtbas  20996  txcls  21407  txlm  21451  qtoptop2  21502  qtoprest  21520  kqt0lem  21539  ptuncnv  21610  fmfnfmlem4  21761  alexsubALTlem2  21852  tgpmulg  21897  blin  22226  xmeter  22238  xmetresbl  22242  dscmet  22377  nmdvr  22474  metnrmlem3  22664  icccvx  22749  bndth  22757  htpycc  22779  pcohtpylem  22819  pi1blem  22839  lmmbrf  23060  iscfil2  23064  iscau4  23077  minveclem7  23206  elovolm  23243  dyaddisjlem  23363  ismbfd  23407  itg1mulc  23471  dvlip  23756  dvcvx  23783  plypf1  23968  eff1olem  24294  logccv  24409  lawcos  24546  sqff1o  24908  dvdsppwf1o  24912  dvdsflf1o  24913  fsumdvdsmul  24921  sgmmul  24926  fsumvma  24938  bposlem6  25014  lgsdchr  25080  rpvmasum2  25201  pntpbnd1  25275  ostthlem1  25316  tgbtwntriv2  25382  ercgrg  25412  hlpasch  25648  colhp  25662  colinearalglem4  25789  axlowdimlem15  25836  axcontlem7  25850  axcontlem8  25851  axcontlem10  25853  usgr1v  26148  pthdivtx  26625  grpolcan  27384  nvmf  27500  sspmval  27588  nmosetre  27619  sspph  27710  minvecolem7  27739  hiassdi  27948  shscli  28176  fh1  28477  fh2  28478  cm2j  28479  chscllem2  28497  spansncvi  28511  5oalem2  28514  adjsym  28692  nmopsetretALT  28722  nmfnsetre  28736  cnvadj  28751  cnvunop  28777  unoplin  28779  hmoplin  28801  lnopmi  28859  hmops  28879  hmopm  28880  nmcexi  28885  adjlnop  28945  adjmul  28951  adjadd  28952  opsqrlem1  28999  mdsl0  29169  ssmd2  29171  mdexchi  29194  superpos  29213  chrelat2i  29224  atcvatlem  29244  atcvati  29245  chirredlem1  29249  chirredi  29253  atcvat3i  29255  atcvat4i  29256  mdsymlem3  29264  mdsymlem5  29266  cdj3lem2b  29296  isoun  29479  xrge0infss  29525  ddemeas  30299  fsum2dsub  30685  hgt750lemb  30734  bnj1145  31061  subfacp1lem3  31164  subfacp1lem5  31166  frind  31740  sltres  31815  nodenselem5  31838  nodenselem6  31839  nodense  31842  btwnconn1lem12  32205  colinbtwnle  32225  broutsideof2  32229  lineelsb2  32255  nn0prpwlem  32317  neibastop2lem  32355  tailfb  32372  onsuct0  32440  finxpreclem2  33227  lindsenlbs  33404  poimirlem4  33413  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  ismblfin  33450  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anc  33493  sdclem1  33539  seqpo  33543  sstotbnd  33574  cntotbnd  33595  ismtycnv  33601  ismtyres  33607  heibor  33620  exidreslem  33676  ghomdiv  33691  grpokerinj  33692  rngohomco  33773  rngoisoco  33781  idlsubcl  33822  divrngidl  33827  ispridl2  33837  ispridlc  33869  riotasv3d  34246  omllaw3  34532  omlfh1N  34545  hlrelat2  34689  cvratlem  34707  cvrat  34708  cvrat3  34728  cvrat4  34729  ps-2  34764  elpaddn0  35086  paddss12  35105  pmodlem2  35133  cdleme0cq  35502  cdlemeg49lebilem  35827  cdleme50eq  35829  tendoeq2  36062  tendoex  36263  diameetN  36345  diainN  36346  dvhopN  36405  djajN  36426  dihmeetcl  36634  mapdheq2  37018  fphpdo  37381  pell1234qrne0  37417  pell14qrgt0  37423  pell1qrge1  37434  monotoddzzfi  37507  expmordi  37512  jm2.18  37555  wepwsolem  37612  dnnumch3  37617  dnwech  37618  kelac1  37633  kercvrlsm  37653  dssmapnvod  38314  gsumws3  38499  gsumws4  38500  cncmpmax  39191  fiiuncl  39234  choicefi  39392  fvelima2  39475  mullimc  39848  mullimcf  39855  idlimc  39858  limclner  39883  climleltrp  39908  limsupub  39936  climuzlem  39975  climliminflimsup2  40041  xlimbr  40053  xlimxrre  40057  dfxlim2v  40073  fperdvper  40133  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnprodlem1  40161  stoweidlem27  40244  stoweidlem48  40265  fourierdlem42  40366  fourierdlem63  40386  fourierdlem65  40388  dfsalgen2  40559  subsaliuncl  40576  sge0iunmptlemfi  40630  sge0rpcpnf  40638  iundjiun  40677  psmeasure  40688  ovnsubaddlem2  40785  hoidmvle  40814  ovolval4lem2  40864  ovolval5lem3  40868  smflimlem2  40980  smflimlem3  40981  smflimlem6  40984  smflimmpt  41016  icceuelpart  41372  mgmhmpropd  41785  subsubmgm  41797  srhmsubc  42076  srhmsubcALTV  42094