Theorem 3ad2ant2 807

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (φ → χ)

Assertion

Ref	Expression
3ad2ant2	⊢ ((ψ ⋀ φ ⋀ θ) → χ)

Proof of Theorem 3ad2ant2

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

Syntax hints:   → wi 3   ⋀ w3a 781

This theorem is referenced by:  mopick2 1476  fnco 3701  oprssoprv 4095  onfununi 4209  onopriun 4211  omass 4347  nnacda 5090  cnegexlem2 5500  xrre2 5724  divne0b 5874  lt2mul2divOLD 6017  lediv2 6036  nndivtr 6106  supxrun 6253  zdivmul 6358  gtndiv 6364  qbtwnre 6418  modabs 6473  modcyc 6475  moddi 6479  modsubdir 6480  ubicc2 6532  icoshftf1olem 6537  eluzp1p1 6562  peano2uz 6574  seqzm1 6744  seqzval2 6748  expnbnd 6852  digit2 6855  absrpcl 7057  seq1ubi 7115  bccmpl 7165  climrecl 7313  geoisum1c 7450  cvgratlem2ALT 7453  cvgratlem2 7456  cvgratlem5 7459  tgtop11 7846  tgss 7848  iincld 7889  elnei 7935  cnconst 7990  metcnpf 8094  metcnp 8098  metdnsconst 8112  caussi 8165  bcthlem9 8218  gxmodid 8335  resgrprn 8336  nvsge0 8538  nvcnpf 8575  nvcnpi3 8676  nvcnpi4 8677  nmoub2i 8691  isblo3i 8716  ipassr2 8763  efifolem5 8998  bcs2 9325  elspansn2 9766  fh2 9838  pjoi0 9940  adjeq 10139  leopmul 10347  mdslmd4i 10541  cdj3lem2 10644  ghomfo 10676  ghomid 10679  nndivsub 10706  seqzp2 10918  truni1 10999  truni3 11001  homcard 11045  hmeobc 11048  filintf 11081  fgsb 11082  fgsb2 11086  rcfpfillem6 11094  altretop 11144  mslb1 11152  2wsms 11153  idosd 11198  dmrngcmp 11205  1cat 11213  imonclem 11268  cmpmon 11270  icmpmon 11271  idmon 11272  isepic 11279  issubcat 11299  morsubc 11309  idsubfun 11312  elfiun 11421  inficlALT 11424  ordtypelem3 11429  ntrin 11463  hausnei2 11471  subsubtop 11479  compsublem 11487  cptclsscpt 11489  hscptsscld 11491  cncomp 11494  alexsublem3 11498  alexsublem4 11499  connsub 11502  subtopmet 11506  reconnlem4 11510  ivthALT 11515  fness 11552  topfne 11561  refssfne 11565  finlocfin 11570  locfincf 11577  comppfsc 11578  neibastop1 11579  topmtcl 11586  ist1-3 11604  fgss 11634  fbfgss 11640  filufint 11659  ufinffr 11663  filcon 11665  ufcondr 11666  fbaslim 11680  limfilcf 11683  hausfillim 11685  cnpfillim 11686  elfilmap 11690  elfilmap2 11691  elfilmap3 11692  fbfgfmeq 11697  rnelfmlem 11698  rnelfm 11699  fmfnfmlem3 11702  fmfnfmlem4 11703  fmfnfm 11704  fmufil 11705  filfm 11706  sflimf 11708  isflimf 11709  flimfnei 11710  flimfbas 11713  flimfcnp 11714  sfcls 11716  filclus 11717  fclusbas 11722  fcluscf 11724  flimfcls 11725  fclsfnflim 11726  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fcluscomplem 11732  fcluscomp 11733  isfclusf 11737  uffcfflf 11742  isga 11772  gafo 11773  ssga 11777  f1ocan1fv 11816  f1ocan2fv 11817  upxp 11822  upixp 11823  fimax 11837  indexf 11847  filbcmb 11857  fsumlt1 11894  incld 11899  neificl 11904  mettrifi2 11913  geomcau 11914  iccsplit 11919  iccss 11920  ismtybndlem 12008

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  df-3an 783

Copyright terms: Public domain