Theorem adantrl 728

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  ad2ant2l  758  ad2ant2rl  761  cases2ALT  1063  consensus  1067  3ad2antr2  1207  3ad2antr3  1208  po2ne  5584  opabssxpd  5707  frpoind  6343  ordelord  6382  f1un  6841  fvelima2  6933  f1cofveqaeqALT  7256  isocnv  7328  isores2  7331  f1oiso2  7350  offval  7685  ordsucun  7819  xp2nd  8017  2ndconst  8094  sexp2  8140  smoord  8350  tfrlem9  8370  tfrlem11  8373  oaass  8544  omordi  8549  omwordri  8555  odi  8562  oewordri  8576  nnawordi  8605  nnmordi  8615  coflton  8655  dom2lem  8987  fundmen  9026  sbthlem9  9081  mapen  9127  mapunen  9132  ssenen  9137  domfi  9171  mapfien  9366  inf3lem6  9600  ttrclselem2  9693  frind  9720  r1val1  9756  rankval3b  9796  numacn  10040  infxpabs  10201  infxp  10204  cfsmolem  10260  infpssrlem4  10296  fin23lem27  10318  isf34lem4  10367  hsmexlem2  10417  axdc3lem2  10441  axdc3lem4  10443  iundom2g  10530  gchen1  10616  fpwwe2lem6  10627  fpwwe2lem10  10631  fpwwe2lem11  10632  prlem936  11038  muladd  11652  leord1  11747  eqord1  11748  ltord2  11749  leord2  11750  eqord2  11751  divadddiv  11936  ltmul12a  12077  lemul12b  12078  fimaxre  12165  supadd  12189  supmullem1  12191  cju  12220  zextlt  12676  zmax  12975  xrre  13201  supxr  13345  ixxdisj  13393  iooshf  13459  icodisj  13509  ioojoin  13516  iccshftr  13519  iccshftl  13521  iccdil  13523  icccntr  13525  iccf1o  13529  fzaddel  13593  fzsubel  13595  modadd1  13948  modmul1  13967  seqcaopr  14082  expsub  14153  expmordi  14210  sqlecan  14252  facndiv  14331  hashss  14452  hashfacen  14498  hashf1lem1  14499  fi1uzind  14551  brfi1indALT  14554  ccatpfx  14745  swrdccatfn  14768  swrdccatin2  14773  2cshwcshw  14869  resqrex  15308  fprodeq0  16036  lcmdvds  16672  hashdvds  16840  eulerthlem2  16847  pceu  16912  pcqcl  16922  infpnlem1  16976  4sqlem11  17021  ramcl  17095  prmgaplem5  17121  imasvscafn  17597  invfun  17827  initoeu2lem2  18078  catcisolem  18173  funcestrcsetclem8  18209  fullestrcsetc  18213  embedsetcestrclem  18219  funcsetcestrclem8  18224  fullsetcestrc  18228  prfcl  18265  prf1st  18266  prf2nd  18267  1st2ndprf  18268  curfuncf  18300  ipodrsfi  18601  mgmhmpropd  18762  subsubmgm  18774  mhmpropd  18856  subsubm  18881  pwsdiagmhm  18896  frmdgsum  18927  grplcan  19073  grplmulf1o  19085  grpraddf1o  19086  dfgrp3lem  19110  mulgsubcl  19160  subsubg  19222  eqger  19252  qus0subgadd  19276  resghm  19308  conjghm  19325  orbsta  19389  psgnunilem2  19571  odmulg  19632  sylow2a  19695  sylow3lem1  19703  lsmssv  19719  pj1ghm  19779  frgpup1  19851  ghmplusg  19922  subsubrng  20673  subsubrg  20708  srhmsubc  20790  issrngd  20969  lmhmco  21175  lmhmf1o  21178  lmhmima  21179  lmhmpreima  21180  reslmhm  21184  pwsdiaglmhm  21189  pwssplit2  21192  pwssplit3  21193  pj1lmhm  21232  lspdisj  21260  rngqiprngghmlem2  21439  rngqiprngghm  21450  prmirred  21635  cygznlem3  21730  frlmsslsp  21957  frlmlbs  21958  frlmup1  21959  issubassa2  22053  psrbagconf1o  22090  psrgrp  22117  evlslem2  22241  evlslem1  22244  evlsvvval  22255  ply1sclf1  22461  mamuass  22570  dmatmul  22665  dmatsubcl  22666  dmatmulcl  22668  dmatcrng  22670  scmatcrng  22689  mdetunilem9  22788  pm2mpghm  22984  fvmptnn04ifb  23019  toponmre  23261  neiptopreu  23301  ordtbas  23360  txcls  23772  txlm  23816  qtoptop2  23867  qtoprest  23885  kqt0lem  23904  ptuncnv  23975  fmfnfmlem4  24125  alexsubALTlem2  24216  tgpmulg  24261  blin  24589  xmeter  24601  xmetresbl  24605  dscmet  24740  nmdvr  24838  metnrmlem3  25030  icccvx  25120  bndth  25128  htpycc  25150  pcohtpylem  25189  pi1blem  25209  lmmbrf  25432  iscfil2  25436  iscau4  25449  minveclem7  25605  elovolm  25645  dyaddisjlem  25765  ismbfd  25809  itg1mulc  25874  dvlip  26163  dvcvx  26190  plypf1  26380  eff1olem  26724  logccv  26839  lawcos  26992  leibpilem1  27116  sqff1o  27357  dvdsppwf1o  27361  dvdsflf1o  27362  fsumdvdsmul  27370  sgmmul  27376  fsumvma  27388  bposlem6  27464  lgsdchr  27530  rpvmasum2  27687  pntpbnd1  27761  ostthlem1  27802  ltsres  27837  nodenselem5  27863  nodenselem6  27864  nodense  27867  addsproplem2  28174  mulsuniflem  28353  mulsunif2lem  28373  precsexlem9  28419  precsexlem10  28420  precsexlem11  28421  om2noseqlt2  28504  om2noseqf1o  28505  z12sge0  28687  elreno2  28699  tgbtwntriv2  28767  ercgrg  28797  hlpasch  29049  colinearalglem4  29270  axlowdimlem15  29317  axcontlem7  29331  axcontlem8  29332  axcontlem10  29334  usgr1v  29617  pthdivtx  30087  clwwlkn1loopb  30405  grpolcan  30893  nvmf  31008  sspmval  31096  nmosetre  31127  minvecolem7  31246  hiassdi  31454  shscli  31680  fh1  31981  fh2  31982  cm2j  31983  chscllem2  32001  spansncvi  32015  5oalem2  32018  adjsym  32196  nmopsetretALT  32226  nmfnsetre  32240  cnvadj  32255  cnvunop  32281  unoplin  32283  hmoplin  32305  lnopmi  32363  hmops  32383  hmopm  32384  nmcexi  32389  adjlnop  32449  adjmul  32455  adjadd  32456  opsqrlem1  32503  mdsl0  32673  ssmd2  32675  mdexchi  32698  superpos  32717  chrelat2i  32728  atcvatlem  32748  atcvati  32749  chirredlem1  32753  chirredi  32757  atcvat3i  32759  atcvat4i  32760  mdsymlem3  32768  mdsymlem5  32770  cdj3lem2b  32800  ifnebib  32906  isoun  33058  xrge0infss  33116  1arithufdlem3  33845  extdg1id  34065  ddemeas  34635  fsum2dsub  35003  hgt750lemb  35052  bnj1145  35390  subfacp1lem3  35682  subfacp1lem5  35684  cvxpconn  35742  satfv1lem  35862  btwnconn1lem12  36598  colinbtwnle  36618  broutsideof2  36622  lineelsb2  36648  nadddilem2  36721  nadddilem4  36723  nn0prpwlem  36861  neibastop2lem  36899  tailfb  36916  onsuct0  36980  finxpreclem2  38064  lindsenlbs  38294  poimirlem4  38303  poimirlem26  38325  poimirlem27  38326  poimirlem31  38330  heicant  38334  mblfinlem2  38337  mblfinlem3  38338  ismblfin  38340  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anc  38380  sdclem1  38422  seqpo  38426  sstotbnd  38454  cntotbnd  38475  ismtycnv  38481  ismtyres  38487  heibor  38500  exidreslem  38556  ghomdiv  38571  grpokerinj  38572  rngohomco  38653  rngoisoco  38661  idlsubcl  38702  divrngidl  38707  ispridl2  38717  ispridlc  38749  riotasv3d  39762  omllaw3  40047  omlfh1N  40060  hlrelat2  40205  cvratlem  40223  cvrat  40224  cvrat3  40244  cvrat4  40245  ps-2  40280  elpaddn0  40602  paddss12  40621  pmodlem2  40649  cdleme0cq  41017  cdlemeg49lebilem  41341  cdleme50eq  41343  tendoeq2  41576  tendoex  41777  diameetN  41858  diainN  41859  dvhopN  41918  djajN  41939  dihmeetcl  42147  mapdheq2  42531  3factsumint1  42816  imacrhmcl  43316  psrmnd  43339  evlselvlem  43348  fsuppind  43350  0prjspn  43388  fphpdo  43572  pell1234qrne0  43608  pell14qrgt0  43614  pell1qrge1  43625  monotoddzzfi  43697  jm2.18  43743  wepwsolem  43797  dnnumch3  43802  dnwech  43803  kelac1  43818  kercvrlsm  43838  onov0suclim  44029  cantnfresb  44079  dssmapnvod  44774  gsumws3  44950  gsumws4  44951  mnuprdlem1  45010  mnuprdlem2  45011  traxext  45714  modelac8prim  45729  cncmpmax  45780  fiiuncl  45813  choicefi  45945  mullimc  46360  mullimcf  46367  idlimc  46370  limclner  46393  climleltrp  46418  limsupub  46446  climuzlem  46485  climliminflimsup2  46551  xlimbr  46569  xlimxrre  46573  dfxlim2v  46589  fperdvper  46661  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  dvnprodlem1  46688  stoweidlem27  46769  stoweidlem48  46790  fourierdlem42  46891  fourierdlem63  46911  fourierdlem65  46913  dfsalgen2  47083  subsaliuncl  47100  sge0iunmptlemfi  47155  sge0rpcpnf  47163  iundjiun  47202  psmeasure  47213  ovnsubaddlem2  47313  hoidmvle  47342  ovolval4lem2  47392  smflimlem2  47514  smflimlem3  47515  smflimlem6  47518  smflimmpt  47552  fcoresf1  47834  icceuelpart  48213  gpgedgvtx0  48854  gpgedgvtx1  48855  srhmsubcALTV  49118  catprs  49817  thincciso2  50261  functermclem  50313  functermc  50314  fulltermc  50317