Theorem adantrl 716

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad2ant2l  746  ad2ant2rl  749  cases2ALT  1049  consensus  1053  3ad2antr2  1190  3ad2antr3  1191  po2ne  5608  opabssxpd  5732  frpoind  6363  wfiOLD  6372  ordelord  6406  f1un  6868  fvelima2  6961  f1cofveqaeqALT  7279  isocnv  7350  isores2  7353  f1oiso2  7372  offval  7706  ordsucun  7845  xp2nd  8047  2ndconst  8126  sexp2  8171  wfrdmclOLD  8357  smoord  8405  tfrlem9  8425  tfrlem11  8428  oaass  8599  omordi  8604  omwordri  8610  odi  8617  oewordri  8630  nnawordi  8659  nnmordi  8669  coflton  8709  dom2lem  9032  fundmen  9071  sbthlem9  9131  mapen  9181  mapunen  9186  ssenen  9191  domfi  9229  mapfien  9448  inf3lem6  9673  ttrclselem2  9766  frind  9790  r1val1  9826  rankval3b  9866  numacn  10089  infxpabs  10251  infxp  10254  cfsmolem  10310  infpssrlem4  10346  fin23lem27  10368  isf34lem4  10417  hsmexlem2  10467  axdc3lem2  10491  axdc3lem4  10493  iundom2g  10580  gchen1  10665  fpwwe2lem6  10676  fpwwe2lem10  10680  fpwwe2lem11  10681  prlem936  11087  muladd  11695  leord1  11790  eqord1  11791  ltord2  11792  leord2  11793  eqord2  11794  divadddiv  11982  ltmul12a  12123  lemul12b  12124  fimaxre  12212  supadd  12236  supmullem1  12238  cju  12262  zextlt  12692  zmax  12987  xrre  13211  supxr  13355  ixxdisj  13402  iooshf  13466  icodisj  13516  ioojoin  13523  iccshftr  13526  iccshftl  13528  iccdil  13530  icccntr  13532  iccf1o  13536  fzaddel  13598  fzsubel  13600  modadd1  13948  modmul1  13965  seqcaopr  14080  expsub  14151  expmordi  14207  sqlecan  14248  facndiv  14327  hashss  14448  hashfacen  14493  hashf1lem1  14494  fi1uzind  14546  brfi1indALT  14549  ccatpfx  14739  swrdccatfn  14762  swrdccatin2  14767  2cshwcshw  14864  resqrex  15289  fprodeq0  16011  lcmdvds  16645  hashdvds  16812  eulerthlem2  16819  pceu  16884  pcqcl  16894  infpnlem1  16948  4sqlem11  16993  ramcl  17067  prmgaplem5  17093  imasvscafn  17582  invfun  17808  initoeu2lem2  18060  catcisolem  18155  funcestrcsetclem8  18192  fullestrcsetc  18196  embedsetcestrclem  18202  funcsetcestrclem8  18207  fullsetcestrc  18211  prfcl  18248  prf1st  18249  prf2nd  18250  1st2ndprf  18251  curfuncf  18283  ipodrsfi  18584  mgmhmpropd  18711  subsubmgm  18723  mhmpropd  18805  subsubm  18829  pwsdiagmhm  18844  frmdgsum  18875  grplcan  19018  grplmulf1o  19031  grpraddf1o  19032  dfgrp3lem  19056  mulgsubcl  19106  subsubg  19167  eqger  19196  qus0subgadd  19217  resghm  19250  conjghm  19267  orbsta  19331  psgnunilem2  19513  odmulg  19574  sylow2a  19637  sylow3lem1  19645  lsmssv  19661  pj1ghm  19721  frgpup1  19793  ghmplusg  19864  subsubrng  20563  subsubrg  20598  srhmsubc  20680  issrngd  20856  lmhmco  21042  lmhmf1o  21045  lmhmima  21046  lmhmpreima  21047  reslmhm  21051  pwsdiaglmhm  21056  pwssplit2  21059  pwssplit3  21060  pj1lmhm  21099  lspdisj  21127  rngqiprngghmlem2  21298  rngqiprngghm  21309  prmirred  21485  cygznlem3  21588  frlmsslsp  21816  frlmlbs  21817  frlmup1  21818  issubassa2  21912  psrbagconf1o  21949  psrgrp  21976  evlslem2  22103  evlslem1  22106  ply1sclf1  22292  mamuass  22406  dmatmul  22503  dmatsubcl  22504  dmatmulcl  22506  dmatcrng  22508  scmatcrng  22527  mdetunilem9  22626  pm2mpghm  22822  fvmptnn04ifb  22857  toponmre  23101  neiptopreu  23141  ordtbas  23200  txcls  23612  txlm  23656  qtoptop2  23707  qtoprest  23725  kqt0lem  23744  ptuncnv  23815  fmfnfmlem4  23965  alexsubALTlem2  24056  tgpmulg  24101  blin  24431  xmeter  24443  xmetresbl  24447  dscmet  24585  nmdvr  24691  metnrmlem3  24883  icccvx  24981  bndth  24990  htpycc  25012  pcohtpylem  25052  pi1blem  25072  lmmbrf  25296  iscfil2  25300  iscau4  25313  minveclem7  25469  elovolm  25510  dyaddisjlem  25630  ismbfd  25674  itg1mulc  25739  dvlip  26032  dvcvx  26059  plypf1  26251  eff1olem  26590  logccv  26705  lawcos  26859  leibpilem1  26983  sqff1o  27225  dvdsppwf1o  27229  dvdsflf1o  27230  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  sgmmul  27245  fsumvma  27257  bposlem6  27333  lgsdchr  27399  rpvmasum2  27556  pntpbnd1  27630  ostthlem1  27671  sltres  27707  nodenselem5  27733  nodenselem6  27734  nodense  27737  addsproplem2  28003  mulsuniflem  28175  mulsunif2lem  28195  precsexlem9  28239  precsexlem10  28240  precsexlem11  28241  om2noseqlt2  28306  om2noseqf1o  28307  tgbtwntriv2  28495  ercgrg  28525  hlpasch  28764  colinearalglem4  28924  axlowdimlem15  28971  axcontlem7  28985  axcontlem8  28986  axcontlem10  28988  usgr1v  29273  pthdivtx  29747  clwwlkn1loopb  30062  grpolcan  30549  nvmf  30664  sspmval  30752  nmosetre  30783  minvecolem7  30902  hiassdi  31110  shscli  31336  fh1  31637  fh2  31638  cm2j  31639  chscllem2  31657  spansncvi  31671  5oalem2  31674  adjsym  31852  nmopsetretALT  31882  nmfnsetre  31896  cnvadj  31911  cnvunop  31937  unoplin  31939  hmoplin  31961  lnopmi  32019  hmops  32039  hmopm  32040  nmcexi  32045  adjlnop  32105  adjmul  32111  adjadd  32112  opsqrlem1  32159  mdsl0  32329  ssmd2  32331  mdexchi  32354  superpos  32373  chrelat2i  32384  atcvatlem  32404  atcvati  32405  chirredlem1  32409  chirredi  32413  atcvat3i  32415  atcvat4i  32416  mdsymlem3  32424  mdsymlem5  32426  cdj3lem2b  32456  ifnebib  32562  isoun  32711  xrge0infss  32764  1arithufdlem3  33574  extdg1id  33716  ddemeas  34237  fsum2dsub  34622  hgt750lemb  34671  bnj1145  35007  subfacp1lem3  35187  subfacp1lem5  35189  cvxpconn  35247  satfv1lem  35367  btwnconn1lem12  36099  colinbtwnle  36119  broutsideof2  36123  lineelsb2  36149  nn0prpwlem  36323  neibastop2lem  36361  tailfb  36378  onsuct0  36442  finxpreclem2  37391  lindsenlbs  37622  poimirlem4  37631  poimirlem26  37653  poimirlem27  37654  poimirlem31  37658  heicant  37662  mblfinlem2  37665  mblfinlem3  37666  ismblfin  37668  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anc  37708  sdclem1  37750  seqpo  37754  sstotbnd  37782  cntotbnd  37803  ismtycnv  37809  ismtyres  37815  heibor  37828  exidreslem  37884  ghomdiv  37899  grpokerinj  37900  rngohomco  37981  rngoisoco  37989  idlsubcl  38030  divrngidl  38035  ispridl2  38045  ispridlc  38077  riotasv3d  38961  omllaw3  39246  omlfh1N  39259  hlrelat2  39405  cvratlem  39423  cvrat  39424  cvrat3  39444  cvrat4  39445  ps-2  39480  elpaddn0  39802  paddss12  39821  pmodlem2  39849  cdleme0cq  40217  cdlemeg49lebilem  40541  cdleme50eq  40543  tendoeq2  40776  tendoex  40977  diameetN  41058  diainN  41059  dvhopN  41118  djajN  41139  dihmeetcl  41347  mapdheq2  41731  3factsumint1  42022  metakunt16  42221  imacrhmcl  42524  psrmnd  42555  evlsvvval  42573  evlselvlem  42596  fsuppind  42600  0prjspn  42638  fphpdo  42828  pell1234qrne0  42864  pell14qrgt0  42870  pell1qrge1  42881  monotoddzzfi  42954  jm2.18  43000  wepwsolem  43054  dnnumch3  43059  dnwech  43060  kelac1  43075  kercvrlsm  43095  onov0suclim  43287  cantnfresb  43337  dssmapnvod  44033  gsumws3  44209  gsumws4  44210  mnuprdlem1  44291  mnuprdlem2  44292  traxext  44994  modelac8prim  45009  cncmpmax  45037  fiiuncl  45070  choicefi  45205  mullimc  45631  mullimcf  45638  idlimc  45641  limclner  45666  climleltrp  45691  limsupub  45719  climuzlem  45758  climliminflimsup2  45824  xlimbr  45842  xlimxrre  45846  dfxlim2v  45862  fperdvper  45934  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnprodlem1  45961  stoweidlem27  46042  stoweidlem48  46063  fourierdlem42  46164  fourierdlem63  46184  fourierdlem65  46186  dfsalgen2  46356  subsaliuncl  46373  sge0iunmptlemfi  46428  sge0rpcpnf  46436  iundjiun  46475  psmeasure  46486  ovnsubaddlem2  46586  hoidmvle  46615  ovolval4lem2  46665  smflimlem2  46787  smflimlem3  46788  smflimlem6  46791  smflimmpt  46825  fcoresf1  47081  icceuelpart  47423  gpgedgvtx0  48019  gpgedgvtx1  48020  srhmsubcALTV  48241  catprs  48900  thincciso2  49104  functermclem  49139  functermc  49140  fulltermc  49143