Theorem ad2antll 407

Description: Deduction adding conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant.1	⊢ (φ → ψ)

Assertion

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

Proof of Theorem ad2antll

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

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  simprr 415  ax11eq 1402  ax11el 1403  ordsucelsuc 3178  funfvima3 3968  isomin 4013  1stconst 4190  oalimcl 4330  odi 4346  pw2en 4587  ac6sfilem3 4590  rankxplim3 4860  axacndlem5 5117  axacnd 5118  divadddiv 5923  lt2mul2div 6016  uzwo4OLD 6381  modmul1 6478  iooshf 6522  uzwo 6582  uzwoOLD 6583  exprec 6789  exprecOLD 6790  replim 6962  climaddlem3 7319  climmullem4 7326  fsum0diaglem2 7462  tgcl 7836  tgss2 7849  neindisj 7941  dnsconst 7998  opni3 8076  lmcau 8207  grpidinvlem1 8261  grprcan 8280  sspval 8636  ubthlem3 8789  ubthlem4 8790  ubthlem12 8798  ubthlem12OLD 8799  minveclem31 8835  minveclem32 8836  hvmulcan2 9216  chocunii 9448  shscli 9557  spansneleq 9769  pjspansn 9776  osumlem7 9862  3oalem2 9886  eigposi 10042  cnlnadjlem2 10280  stlesi 10449  mdslmd1lem1 10533  mdslmd1lem2 10534  cdj1i 10642  trnij 11160  codcmpd 11201  cmpidb 11229  imonclem 11268  cmpmon 11270  simprrl 11368  simprrr 11369  finminlem 11418  fictblem 11422  fictb 11423  ordiso 11426  hartoglem 11435  hartog 11436  omsubsuc2 11439  cnpnei 11472  elsubsp 11477  subcls 11481  subntr 11482  cnsubsp2 11484  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  subtopmet 11506  reconnlem1 11507  reconnlem4 11510  2ndcctbss 11539  isfne3 11543  fnetr 11556  reftr 11558  topfneec 11562  fnessref 11564  refssfne 11565  locfincomp 11575  comppfsc 11578  neibastop2lem4 11583  topmeet 11587  topjoin 11588  fnemeet1 11589  ist1-2 11603  isnrm2 11613  fbunfip 11631  extbas1 11641  filrn 11643  supfil 11645  filfinnfr 11646  isufil2 11650  filssufillem 11655  filssufil 11656  uffixfr 11660  fixufil 11661  ufinffr 11663  limfilcf 11683  cnpfillim 11686  elfilmap2 11691  fmfnfmlem2 11701  fmfnfmlem3 11702  fmfnfmlem4 11703  fmufil 11705  fclusnei 11719  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  isfclusf 11737  fclusfnei 11738  dirtr 11753  filnetlem1 11763  filnetlem3 11765  filnetlem4 11766  gapmlem 11783  inficl 11849  frinfm 11850  sdc 11877  subspopn 11900  subspcld 11901  neificl 11904  blssp 11908  metsstop 11909  mettrifi 11912  lincmb01icc 11943  addccncf 11945  sub1cncf 11946  sub2cncf 11947  txsubsp 11983  sstotbnd 11992  isbnd3 11997  ismtyhmeolem 12006  ismtybndlem 12008  ismtyres 12010  heiborlem36 12046  rrndstprj 12073  rrntotbndlem1 12076  rrntotbndlem2 12077

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