Theorem ad2antlr 405

Description: Deduction adding conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant.1	⊢ (φ → ψ)

Assertion

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

Proof of Theorem ad2antlr

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

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  simplr 413  ax11eq 1402  ax11el 1403  tfindsg 3213  caoprord3 4119  oesuc 4302  oelim 4305  oaordi 4316  oaass 4331  odi 4346  omass 4347  oen0 4349  oelim2 4358  undom 4579  xpdom2 4583  mapenlem1 4636  mapenlem2 4637  php3 4662  fiint 4703  suppr 4733  fodom 4944  unxpdomlem 4993  npex 5245  elnp 5246  cnegex 5502  lemul12a 5988  lt2mul2divOLD 6017  lediv12a 6041  lediv2a 6042  xrmax2 6055  xrsupsslem 6244  xrinfmsslem 6245  xrub 6248  supxrre 6251  supxrun 6253  supxrunb1 6257  supxrunb2 6258  supxrbnd 6259  modid 6471  monoord 6482  elioc2 6516  elico2 6517  elicc2 6518  elfzp1 6641  fsequb 6654  expnlbnd2 6854  sqr11i 6904  absmax 7100  seq1bndi 7113  cvganz 7127  caubndi 7129  facndiv 7146  faclbnd 7148  sumeq2 7188  fsumcmpndx2 7245  2climnn 7305  2climnn0 7306  climrecl 7313  climsqueeze 7343  climsqueeze2 7344  climsupi 7358  climcaui 7359  caucvglem6 7365  caucvgi 7366  reccnv 7422  cvgratlem2 7456  cvgratlem3 7457  fsum0diaglem2 7462  fsum0diag4 7466  acdc3lem 7697  acdc2lem2 7701  acdc5lem2 7704  acdclem 7706  infxpidmlem12 7775  basgen2 7851  elcls3 7921  islp2 7957  iscnp2 7971  cnpco 7979  blss 8063  metequiv 8091  metcnplem 8097  metcnp 8098  metcni2 8106  metcnp3 8107  metcnss2 8110  tgioolem 8125  lmnn 8146  metcnp4lem2 8180  metcn4 8182  xpcn 8187  bcthlem2 8211  bcthlem13 8222  bcthlem14 8223  bcthlem27 8236  bcthlem28 8237  grpidinv 8265  grpideu 8266  isgrp2i 8293  nvmul0or 8519  vacnlem3 8584  sm1cnilem 8601  sspval 8636  nmoub3i 8690  nmo0 8706  blocnilem 8719  blocni 8720  ipblnfi 8772  ubthlem3 8789  ubthlem5 8791  ubthlem13 8800  ubthlem13OLD 8801  minveclem27 8831  minveclem31 8835  hvmul0or 9169  hvmulcan 9214  hvaddsub4 9221  occon 9436  ocorth 9440  occllem6 9454  projlem25 9486  osumlem4 9859  5oalem1 9877  5oalem2 9878  3oalem2 9886  pjds3i 9936  nmopub2tALT 10113  nmfnleub2 10130  hmopadj2 10145  lnopconi 10242  lnfnconi 10269  nlelchi 10273  cnlnadjlem6 10284  kbass5 10333  leopnmid 10351  nmopleid 10352  hmopidmchi 10359  pjss2coi 10372  pjssdif1i 10383  pj3cor1i 10418  mdsl0 10518  mdslmd1lem1 10533  mdslmd1lem2 10534  csmdsymi 10542  superpos 10562  atomli 10591  irredlem2 10600  irredlem3 10601  atcvat3i 10605  atcvat4i 10606  mdsymlem5 10616  cdjreui 10641  cdj1i 10642  cdrci 10994  cnrsfin 11012  cnrscoa 11013  mapdiscn 11014  osneisi 11018  sfvlim 11100  iintlem1 11155  trnij 11160  cmpasso 11227  idsubfun 11312  simplrl 11364  simplrr 11365  elicc3 11410  ioodisj 11413  finminlem 11418  elfiun 11421  fictblem 11422  finsschain 11425  ordiso 11426  ordtypelem5 11431  ordtypelem6 11432  ordtypelem7 11433  hartoglem 11435  hartog 11436  cnpnei 11472  subcld 11480  cnsubsp 11483  cnsubsp2 11484  compsublem 11487  compsub 11488  cptclsscpt 11489  uncomp 11490  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  cnconn 11503  subtopmet 11506  2ndcsb 11537  2ndcctbss 11539  refssfne 11565  locfincf 11577  comppfsc 11578  neibastop2lem3 11582  neibastop2 11584  topmeet 11587  fnemeet2 11590  fnejoin2 11592  fbssint 11626  fgfil 11638  fgmin 11639  filrn 11643  isufil2 11650  filssufillem 11655  ufileu 11658  uffixfr 11660  ufilen 11664  flimopn 11679  hausfillim 11685  cnpfillim 11686  rnelfm 11699  fmfnfmlem2 11701  fmfnfm 11704  flimfcnp 11714  fclusnei 11719  fcluscnplem 11729  fcluscnp 11730  dirtr 11753  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  upxp 11822  upixp 11823  fixp 11840  indexf 11847  filbcmb 11857  nnubfi 11881  nninfnub 11882  fsumlt1 11894  blssp 11908  mettrifi2 11913  geomcau 11914  metdcn 11918  iccsplit 11919  iocopnst 11941  lincmb01icc 11943  cnss 11953  tx1cn 11976  txcn 11979  2txcn 11982  txcld 11985  sstotbnd 11992  totbndss 11993  totbndbnd 12000  ismtyhmeolem 12006  heiborlem12 12022  heiborlem16 12026  heiborlem32 12042  heiborlem35 12045  heiborlem36 12046  rrndstprj2 12074  rrncms 12075  rrntotbndlem1 12076  rrntotbnd 12078  iccbnd 12082  phtpycom 12092

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