Theorem ad2antrl 406

Description: Deduction adding conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant.1	⊢ (φ → ψ)

Assertion

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

Proof of Theorem ad2antrl

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

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  simprl 414  tz7.7 3001  onint 3152  elxp5 3586  tz7.48lem 4256  oalimcl 4330  ac6sfilem3 4590  sdomdomtr 4614  mapenlem2 4637  mapunen 4649  fodomfi 4709  aceq3 4879  aceq5 4886  axacnd 5118  ltapq 5230  ltexprlem7 5302  cnegexlem2 5500  divadddiv 5923  divdiv1 5934  divdiv2 5935  conjmul 5937  ltdivmul 6011  ledivmul 6013  lt2mul2div 6016  lt2mul2divOLD 6017  ltdiv23 6037  lediv23 6038  lediv12a 6041  ledivp1 6050  zltp1le 6349  peano2uz2 6372  uzwo5OLD 6382  uzwo3lem1 6388  modadd1 6477  modmul1 6478  iooshf 6522  ioojoin 6543  eluzp1m1 6560  climrecl 7313  climmullem1 7323  climmullem3 7325  climmullem4 7326  climmullem5 7327  climsupi 7358  caucvglem6 7365  serzf0i 7372  cvgratlem3 7457  cvgratlem5 7459  acdc3lem 7697  acdc2lem2 7701  acdc5lem2 7704  acdclem 7706  infxpidmlem1 7764  tgcl 7836  clsval2 7895  qdensere 7961  cnconst 7990  opnuni 8078  metcnp 8098  metcnpi3 8103  metcnpi4 8104  metcni2 8106  causs 8166  xpcn 8187  cmsss 8208  bcthlem17 8226  grpidinvlem1 8261  grpidinvlem3 8263  grprcan 8280  vcsubdir 8422  vacnlem6 8587  sqcn 8589  nmlnoubi 8711  blocnilem 8719  ubthlem3 8789  ubthlem8 8794  ocsh 9432  projlem26 9487  pjpj0i 9531  shmodsi 9638  osumlem7 9862  5oalem2 9878  3oalem2 9886  eigposi 10042  nmopub2tALT 10113  nmfnleub2 10130  nmcopexlem5 10234  lnopconi 10242  nmcfnexlem5 10263  lnfnconi 10269  nmopcoi 10307  kbass3 10331  mdslmd1lem1 10533  mdslmd1lem2 10534  atom1d 10561  irredlem2 10600  irredlem4 10602  mdsymlem3 10614  mdsymlem5 10616  sumdmdii 10624  sumdmdlem 10627  sumdmdlem2 10628  toplat 10884  ismnd1 10927  isdivrng 10968  qusp 11068  usinuniop 11128  iintlem1 11155  trnij 11160  domcmpd 11200  cmpida 11228  cmpmon 11270  simprll 11366  simprlr 11367  xpss1 11403  xpss2 11404  finminlem 11418  elfiun 11421  inficlALT 11424  ordiso 11426  cnsubsp 11483  cnsubsp2 11484  compsublem 11487  compsub 11488  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  cncomp 11494  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  cnconn 11503  subtopmetlem 11505  reconnlem1 11507  reconnlem4 11510  reconnlem5 11511  ivthALT 11515  2ndcsb 11537  2ndcctbss 11539  topfneec 11562  fnessref 11564  locfincomp 11575  comppfsc 11578  neibastop2lem1 11580  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  topmeet 11587  topjoin 11588  fnejoin1 11591  fbssint 11626  fbunfip 11631  extbas1 11641  filrn 11643  isufil2 11650  filssufillem 11655  ufileu 11658  ufilen 11664  limfilcf 11683  flimcls 11684  hausfillim 11685  elfilmap 11690  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem4 11703  fmufil 11705  fclusnei 11719  fcluscf 11724  fclsfnflim 11726  fcluscnplem 11729  fcluscnp 11730  fclusfnei 11738  dirtr 11753  filnetlem1 11763  filnetlem4 11766  filnetlem5 11767  oprabopabf 11807  upixp 11823  inficl 11849  frinfm 11850  geomcau 11914  metdcn 11918  addccncf 11945  sub1cncf 11946  sub2cncf 11947  cnres 11950  txsubsp 11983  totbndss 11993  ismtyhmeolem 12006  ismtyres 12010  heiborlem23 12033  rrndstprj 12073  rrntotbndlem2 12077  phtpycolem4 12096  phtpcer 12104

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