Theorem adantrl 729

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

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

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 402

This theorem is used by:  ad2ant2l  759  ad2ant2rl  762  cases2ALT  1064  consensus  1068  3ad2antr2  1208  3ad2antr3  1209  po2ne  5575  opabssxpd  5698  frpoind  6344  ordelord  6383  f1un  6843  fvelima2  6935  f1cofveqaeqALT  7260  isocnv  7336  isores2  7339  f1oiso2  7358  offval  7700  ordsucun  7834  xp2nd  8032  2ndconst  8110  sexp2  8156  smoord  8366  tfrlem9  8386  tfrlem11  8389  oaass  8562  omordi  8567  omwordri  8573  odi  8580  oewordri  8594  nnawordi  8623  nnmordi  8633  coflton  8673  dom2lem  9012  fundmen  9052  sbthlem9  9107  mapen  9153  mapunen  9158  ssenen  9163  domfi  9197  mapfien  9393  inf3lem6  9627  ttrclselem2  9720  frind  9747  r1val1  9786  rankval3b  9829  numacn  10121  infxpabs  10282  infxp  10285  cfsmolem  10341  infpssrlem4  10377  fin23lem27  10399  isf34lem4  10448  hsmexlem2  10498  axdc3lem2  10522  axdc3lem4  10524  iundom2g  10617  gchen1  10703  fpwwe2lem6  10714  fpwwe2lem10  10718  fpwwe2lem11  10719  prlem936  11125  muladd  11741  leord1  11836  eqord1  11837  ltord2  11838  leord2  11839  eqord2  11840  divadddiv  12025  ltmul12a  12166  lemul12b  12167  fimaxre  12254  supadd  12278  supmullem1  12280  cju  12309  zextlt  12766  zmax  13065  xrre  13292  supxr  13436  ixxdisj  13484  iooshf  13550  icodisj  13600  ioojoin  13607  iccshftr  13610  iccshftl  13612  iccdil  13614  icccntr  13616  iccf1o  13620  fzaddel  13685  fzsubel  13687  modadd1  14041  modmul1  14060  seqcaopr  14175  expsub  14246  expmordi  14303  sqlecan  14346  facndiv  14425  hashss  14546  hashfacen  14592  hashf1lem1  14593  fi1uzind  14645  brfi1indALT  14648  ccatpfx  14843  swrdccatfn  14866  swrdccatin2  14871  2cshwcshw  14969  resqrex  15410  fprodeq0  16135  lcmdvds  16776  hashdvds  16945  eulerthlem2  16952  pceu  17017  pcqcl  17027  infpnlem1  17081  4sqlem11  17126  ramcl  17200  prmgaplem5  17226  imasvscafn  17702  invfun  17932  initoeu2lem2  18183  catcisolem  18278  funcestrcsetclem8  18314  fullestrcsetc  18318  embedsetcestrclem  18324  funcsetcestrclem8  18329  fullsetcestrc  18333  prfcl  18370  prf1st  18371  prf2nd  18372  1st2ndprf  18373  curfuncf  18405  ipodrsfi  18706  mgmhmpropd  18880  subsubmgm  18892  mhmpropd  18980  subsubm  19005  pwsdiagmhm  19020  frmdgsum  19051  grplcan  19204  grplmulf1o  19216  grpraddf1o  19217  dfgrp3lem  19241  mulgsubcl  19291  subsubg  19353  eqger  19383  qus0subgadd  19407  resghm  19439  conjghm  19456  orbsta  19520  psgnunilem2  19702  odmulg  19763  sylow2a  19826  sylow3lem1  19834  lsmssv  19850  pj1ghm  19910  frgpup1  19982  ghmplusg  20053  subsubrng  20808  subsubrg  20843  srhmsubc  20925  issrngd  21105  lmhmco  21311  lmhmf1o  21314  lmhmima  21315  lmhmpreima  21316  reslmhm  21320  pwsdiaglmhm  21325  pwssplit2  21328  pwssplit3  21329  pj1lmhm  21368  lspdisj  21396  rngqiprngghmlem2  21577  rngqiprngghm  21588  prmirred  21773  cygznlem3  21868  frlmsslsp  22095  frlmlbs  22096  frlmup1  22097  lindsenlbs  22150  issubassa2  22193  psrbagconf1o  22230  psrgrp  22257  evlslem2  22381  evlslem1  22384  evlsvvval  22395  ply1sclf1  22601  mamuass  22710  dmatmul  22805  dmatsubcl  22806  dmatmulcl  22808  dmatcrng  22810  scmatcrng  22829  mdetunilem9  22928  pm2mpghm  23127  fvmptnn04ifb  23162  toponmre  23404  neiptopreu  23444  ordtbas  23503  txcls  23916  txlm  23960  qtoptop2  24011  qtoprest  24029  kqt0lem  24048  ptuncnv  24119  fmfnfmlem4  24269  alexsubALTlem2  24360  tgpmulg  24405  blin  24733  xmeter  24745  xmetresbl  24749  dscmet  24884  nmdvr  24982  metnrmlem3  25174  icccvx  25264  bndth  25272  htpycc  25294  pcohtpylem  25333  pi1blem  25353  lmmbrf  25576  iscfil2  25580  iscau4  25593  minveclem7  25749  elovolm  25789  dyaddisjlem  25909  ismbfd  25953  itg1mulc  26018  dvlip  26306  dvcvx  26333  plypf1  26524  eff1olem  26869  logccv  26984  lawcos  27137  leibpilem1  27261  sqff1o  27502  dvdsppwf1o  27506  dvdsflf1o  27507  fsumdvdsmul  27515  sgmmul  27521  fsumvma  27533  bposlem6  27609  lgsdchr  27675  rpvmasum2  27832  pntpbnd1  27906  ostthlem1  27947  ltsres  28012  nodenselem5  28038  nodenselem6  28039  nodense  28042  addsproplem2  28349  mulsuniflem  28528  mulsunif2lem  28548  precsexlem9  28594  precsexlem10  28595  precsexlem11  28596  om2noseqlt2  28679  om2noseqf1o  28680  z12sge0  28862  elreno2  28874  tgbtwntriv2  28943  ercgrg  28973  hlpasch  29227  colinearalglem4  29480  axlowdimlem15  29527  axcontlem7  29541  axcontlem8  29542  axcontlem10  29544  usgr1v  29830  pthdivtx  30305  clwwlkn1loopb  30627  grpolcan  31125  nvmf  31240  sspmval  31328  nmosetre  31359  minvecolem7  31478  hiassdi  31686  shscli  31912  fh1  32213  fh2  32214  cm2j  32215  chscllem2  32233  spansncvi  32247  5oalem2  32250  adjsym  32428  nmopsetretALT  32458  nmfnsetre  32472  cnvadj  32487  cnvunop  32513  unoplin  32515  hmoplin  32537  lnopmi  32595  hmops  32615  hmopm  32616  nmcexi  32621  adjlnop  32681  adjmul  32687  adjadd  32688  opsqrlem1  32735  mdsl0  32905  ssmd2  32907  mdexchi  32930  superpos  32949  chrelat2i  32960  atcvatlem  32980  atcvati  32981  chirredlem1  32985  chirredi  32989  atcvat3i  32991  atcvat4i  32992  mdsymlem3  33000  mdsymlem5  33002  cdj3lem2b  33032  ifnebib  33138  isoun  33288  xrge0infss  33345  1arithufdlem3  34071  extdg1id  34291  ddemeas  34862  fsum2dsub  35229  hgt750lemb  35278  bnj1145  35616  subfacp1lem3  35926  subfacp1lem5  35928  cvxpconn  35986  satfv1lem  36106  btwnconn1lem12  36843  colinbtwnle  36863  broutsideof2  36867  lineelsb2  36893  nadddilem2  36950  nadddilem4  36952  nn0prpwlem  37090  neibastop2lem  37128  tailfb  37145  onsuct0  37209  finxpreclem2  38293  poimirlem4  38522  poimirlem26  38544  poimirlem27  38545  poimirlem31  38549  heicant  38553  mblfinlem2  38556  mblfinlem3  38557  ismblfin  38559  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anc  38599  sdclem1  38657  seqpo  38661  sstotbnd  38689  cntotbnd  38710  ismtycnv  38716  ismtyres  38722  heibor  38735  exidreslem  38791  ghomdiv  38806  grpokerinj  38807  rngohomco  38888  rngoisoco  38896  idlsubcl  38937  divrngidl  38942  ispridl2  38952  ispridlc  38984  riotasv3d  39997  omllaw3  40282  omlfh1N  40295  hlrelat2  40440  cvratlem  40458  cvrat  40459  cvrat3  40479  cvrat4  40480  ps-2  40515  elpaddn0  40837  paddss12  40856  pmodlem2  40884  cdleme0cq  41252  cdlemeg49lebilem  41576  cdleme50eq  41578  tendoeq2  41811  tendoex  42012  diameetN  42093  diainN  42094  dvhopN  42153  djajN  42174  dihmeetcl  42382  mapdheq2  42766  3factsumint1  43051  imacrhmcl  43561  psrmnd  43587  evlselvlem  43596  fsuppind  43598  0prjspn  43644  fphpdo  43803  pell1234qrne0  43839  pell14qrgt0  43845  pell1qrge1  43856  monotoddzzfi  43928  jm2.18  43974  wepwsolem  44028  dnnumch3  44033  dnwech  44034  kelac1  44049  kercvrlsm  44069  onov0suclim  44260  cantnfresb  44310  dssmapnvod  45005  gsumws3  45181  gsumws4  45182  mnuprdlem1  45241  mnuprdlem2  45242  traxext  45945  modelac8prim  45960  cncmpmax  46018  fiiuncl  46051  choicefi  46183  mullimc  46597  mullimcf  46604  idlimc  46607  limclner  46630  climleltrp  46655  limsupub  46683  climuzlem  46722  climliminflimsup2  46788  xlimbr  46806  xlimxrre  46810  dfxlim2v  46826  fperdvper  46898  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnprodlem1  46925  stoweidlem27  47006  stoweidlem48  47027  fourierdlem42  47128  fourierdlem63  47148  fourierdlem65  47150  dfsalgen2  47320  subsaliuncl  47337  sge0iunmptlemfi  47392  sge0rpcpnf  47400  iundjiun  47439  psmeasure  47450  ovnsubaddlem2  47550  hoidmvle  47579  ovolval4lem2  47629  smflimlem2  47751  smflimlem3  47752  smflimlem6  47755  smflimmpt  47789  fcoresf1  48108  icceuelpart  48487  gpgedgvtx0  49128  gpgedgvtx1  49129  srhmsubcALTV  49391  catprs  50088  thincciso2  50532  functermclem  50584  functermc  50585  fulltermc  50588