Theorem ad2antrr 404

Description: Deduction adding conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant.1	⊢ (φ → ψ)

Assertion

Ref	Expression
ad2antrr	⊢ (((φ ⋀ χ) ⋀ θ) → ψ)

Proof of Theorem ad2antrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (φ → ψ)
2	1	adantr 389	. 2 ⊢ ((φ ⋀ χ) → ψ)
3	2	adantr 389	1 ⊢ (((φ ⋀ χ) ⋀ θ) → ψ)

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  simpll 412  ax11eq 1402  ax11el 1403  ax11indalem 1407  ax11inda2ALT 1408  reupick 2331  tz7.7 3001  reuuniss2 3114  fvelimab 3876  dffo4 3934  onfununi 4209  tz7.49 4260  oaordi 4316  oaass 4331  oarec 4332  omwordri 4339  omword2 4341  omass 4347  oneo 4348  oaabs 4392  nneob 4395  ac6sfilem3 4590  sbthlem8 4599  onomeneq 4665  unblem1 4686  unblem3 4688  fodomfi 4709  suppr 4733  inf3lem5 4762  infensuc 4784  r1ord 4801  ltexpq 5234  genpnnp 5262  addcanpr 5306  prlem936b 5308  supexpr 5317  cnegexlem1 5499  cnegex 5502  xrre 5723  conjmul 5937  lemulge11 5992  ledivp1 6050  xrmin1 6056  lbinfm 6216  xrsupsslem 6244  xrinfmsslem 6245  supxrre 6251  supxrun 6253  supxrunb1 6257  supxrunb2 6258  zltp1le 6349  zbtwnre 6393  btwnzge0 6445  modid 6471  monoord 6482  elioc2 6516  elico2 6517  elicc2 6518  elfzp1 6641  fzneuz 6649  fsequb 6654  ser1add2i 6703  ser1addi 6704  seqzfveq 6749  expnlbnd2 6854  digit1 6856  sqr11i 6904  seq1bndi 7113  cvg2i 7125  cvganz 7127  facndiv 7146  faclbnd 7148  fsumsplit 7223  fsumcmpndx2 7245  clm4lei 7284  climshfti 7307  climmullem3 7325  climsqueeze 7343  climsqueeze2 7344  climsupi 7358  climcaui 7359  caucvgi 7366  ser1cmp2i 7380  isum1p 7410  isummulc1 7416  expcnv 7437  cvgratlem5 7459  fsum0diaglem2 7462  fsum0diag4 7466  ef0lem 7515  tgss2 7849  basgen2 7851  2basgen 7853  cctop 7862  elcls 7914  neips 7937  neissex 7948  cnco 7978  cnpco 7979  iscncl 7980  cnconst 7990  metxp 8044  blval 8047  bl2in 8053  blelrn 8058  blss 8063  ssblex 8066  blopn 8086  neibl 8087  lpbl 8090  metequiv 8091  metcnplem 8097  metcnp 8098  metcnp2 8099  metcnpi3 8103  metcnpi4 8104  metcnss 8109  metcnss2 8110  tgioolem 8125  lmnn 8146  lmuni 8162  lmle 8171  metelcls 8176  metcnp4 8181  metcn4 8182  cmsss 8208  bcthlem2 8211  bcthlem16 8225  bcthlem24 8233  bcthlem26 8235  grpidinvlem3 8263  grprcan 8280  vacnlem3 8584  sm1cnilem 8601  sspval 8636  sspn 8649  nmoub3i 8690  0lno 8705  nmlno0lem 8708  blocnilem 8719  blocni 8720  ipasslem3 8748  ipblnfi 8772  ubthlem10 8796  ubthlem11 8797  ubthlem12 8798  ubthlem12OLD 8799  minveclem24 8828  htthlem6 8887  htthlem7 8888  spwpr4 8925  abssinper 8980  hvaddsub4 9221  sh 9354  occon 9436  chocunii 9448  occllem6 9454  elspansn4 9772  normcan 9775  osumlem6 9861  5oalem1 9877  3oalem2 9886  nmopub2tALT 10113  unoplin 10124  nmfnleub2 10130  hmoplin 10146  nmlnop0iALT 10199  nmcopexlem5 10234  nmophmi 10240  lnopconi 10242  nmcfnexlem5 10263  lnfnconi 10269  nlelchi 10273  cnlnadjlem6 10284  rnbra 10320  kbass4 10332  kbass5 10333  stel 10422  hstel2 10427  mdsl0 10518  mdslmd1lem1 10533  mdslmd1lem2 10534  mdslmd3i 10540  mdexchi 10543  atsseq 10555  atordi 10593  irredlem1 10599  irredlem3 10601  mdsymlem2 10613  mdsymlem3 10614  mdsymlem5 10616  sumdmdii 10624  cdjreui 10641  cdj1i 10642  cdj3lem2b 10646  tostos 10883  toplat 10884  exidu1 10902  cdrci 10994  truni1 10999  cnrsfin 11012  cnrscoa 11013  hmphsyma 11034  qusp 11068  cnfilca 11088  iintlem1 11155  trnij 11160  homgrf 11257  imonclem 11268  ismonc 11269  cmpmon 11270  idmon 11272  isepic 11279  idsubfun 11312  simplll 11362  simpllr 11363  elicc3 11410  ioodisj 11413  finminlem 11418  elfiun 11421  fictblem 11422  finsschain 11425  ordiso 11426  ordtypelem6 11432  ordtypelem7 11433  hartoglem 11435  hartog 11436  omsubsdomlem2 11441  cnpnei 11472  cncls 11473  subsubtop 11479  subcld 11480  cnsubsp 11483  cnsubsp2 11484  compsublem 11487  compsub 11488  cptclsscpt 11489  hscptsscld 11491  alexsublem3 11498  alexsublem4 11499  alexsub 11500  cnconn 11503  subtopmetlem 11505  subtopmet 11506  reconnlem1 11507  reconnlem2 11508  reconnlem3 11509  reconnlem4 11510  reconnlem5 11511  reconn 11512  2ndcsb 11537  2ndcctbss 11539  isfne3 11543  fnetr 11556  topfneec 11562  locfincf 11577  comppfsc 11578  neibastop1 11579  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  topjoin 11588  fnemeet2 11590  fbasfip 11627  fbfgss 11640  filrn 11643  supfil 11645  isufil2 11650  filssufillem 11655  ufileulem 11657  ufileu 11658  uffixfr 11660  fixufil 11661  ufinffr 11663  ufilen 11664  filcon 11665  flimopn 11679  limfilcf 11683  flimcls 11684  hausfillim 11685  cnpfillim 11686  elfilmap3 11692  rnelfmlem 11698  rnelfm 11699  fmfnfmlem1 11700  fmfnfmlem2 11701  fmfnfmlem3 11702  fmfnfmlem4 11703  fmfnfm 11704  fmufil 11705  flimfcnp 11714  isfclus 11718  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fcluscomplem 11732  isfclusf 11737  dirtr 11753  filnetlem4 11766  filnetlem5 11767  filnet 11768  ssga 11777  gapmlem 11783  upixp 11823  indexf 11847  fipreima 11848  filbcmb 11857  sdc 11877  incsequz 11879  nnubfi 11881  nninfnub 11882  fsumlt1 11894  subspabs 11903  blssp 11908  metsstop 11909  mettrifi 11912  geomcau 11914  metdcn 11918  icoopnst 11940  cnimass 11949  cnres 11950  lmtlm 11969  tx2cn 11977  uptx 11978  txcn 11979  2txcn 11982  txsubsp 11983  txcld 11985  sstotbnd 11992  totbndss 11993  isbnd3 11997  bndss 11998  totbndbnd 12000  ismtyhmeolem 12006  ismtybndlem 12008  heiborlem12 12022  heiborlem13 12023  heiborlem16 12026  heiborlem23 12033  heiborlem32 12042  heiborlem34 12044  heiborlem35 12045  heiborlem36 12046  heiborlem42 12052  bfplem9 12062  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  iccbnd 12082  phtpyco 12098

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain