Theorem 3ad2ant3 1022

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	|- ( ph -> ch )

Assertion

Ref	Expression
3ad2ant3	|- ( ( ps /\ th /\ ph ) -> ch )

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantl 277	. 2 |- ( ( th /\ ph ) -> ch )
3	2	3adant1 1017	1 |- ( ( ps /\ th /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simp3l  1027  simp3r  1028  simp31  1035  simp32  1036  simp33  1037  simp3ll  1070  simp3lr  1071  simp3rl  1072  simp3rr  1073  simp3l1  1104  simp3l2  1105  simp3l3  1106  simp3r1  1107  simp3r2  1108  simp3r3  1109  simp31l  1122  simp31r  1123  simp32l  1124  simp32r  1125  simp33l  1126  simp33r  1127  simp311  1146  simp312  1147  simp313  1148  simp321  1149  simp322  1150  simp323  1151  simp331  1152  simp332  1153  simp333  1154  3anim123i  1186  3jaao  1319  ceqsalt  2789  ceqsralt  2790  vtoclgft  2814  ifbothdc  3594  ifnebibdc  3604  tpssi  3789  sotricim  4358  elirr  4577  en2lp  4590  reg3exmidlemwe  4615  sotri2  5067  poltletr  5070  funprg  5308  funtpg  5309  fntpg  5314  funimaexglem  5341  fvun1  5627  ftpg  5746  fsnunf  5762  fsnunfv  5763  caovimo  6117  brtposg  6312  smoel  6358  rdgivallem  6439  frecsuclem  6464  mapxpen  6909  unsnfi  6980  unsnfidcex  6981  unsnfidcel  6982  sbthlemi4  7026  elfir  7039  updjud  7148  ltsopi  7387  distrnqg  7454  ltmnqg  7468  mulcanenq0ec  7512  distrnq0  7526  prarloclem5  7567  1idprl  7657  1idpru  7658  ltaprg  7686  recexprlemopl  7692  recexprlemopu  7694  recexprlem1ssl  7700  aptipr  7708  ltmprr  7709  cauappcvgprlemlol  7714  cauappcvgprlemupu  7716  caucvgprlemlol  7737  caucvgprlemupu  7739  caucvgprprlemlol  7765  caucvgprprlemupu  7767  readdcan  8166  cnegexlem2  8202  addcan2  8207  ltadd2  8446  apreap  8614  ltmul1  8619  apcotr  8634  apadd1  8635  mulext1  8639  divdirap  8724  divcanap5  8741  ltdiv1  8895  lt2halves  9227  zdivmul  9416  eluzsub  9631  ledivge1le  9801  addlelt  9843  xaddass  9944  xleadd1  9950  xltadd1  9951  elioo5  10008  iccsupr  10041  iccneg  10064  icoshft  10065  icoshftf1o  10066  zltaddlt1le  10082  fzen  10118  elfz1b  10165  fzrevral  10180  fzshftral  10183  elfz0ubfz0  10200  elfz0fzfz0  10201  fz0fzelfz0  10202  fz0fzdiffz0  10205  elfzo  10224  fzodcel  10228  elfzonlteqm1  10286  modqaddmulmod  10483  expdivap  10682  leexp2a  10684  bcval3  10843  omgadd  10894  shftfibg  10985  elicc4abs  11259  xrmaxltsup  11423  xrmaxadd  11426  xrlemininf  11436  xrminltinf  11437  mulcn2  11477  fsumsplitsnun  11584  prodfrecap  11711  demoivreALT  11939  dvdsval2  11955  dvdsmodexp  11960  dvdsmulcr  11986  modmulconst  11988  dvdsexp  12026  oddge22np1  12046  modremain  12094  mulgcd  12183  mulgcdr  12185  gcddiv  12186  rpmulgcd  12193  rplpwr  12194  coprmdvds  12260  cncongr1  12271  dvdsnprmd  12293  prmexpb  12319  rpexp  12321  cncongrprm  12325  modprm0  12423  modprmn0modprm0  12425  coprimeprodsq  12426  pythagtriplem1  12434  pythagtriplem3  12436  pythagtriplem10  12438  pythagtriplem6  12439  pythagtriplem11  12443  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem15  12447  pythagtriplem17  12449  pythagtriplem19  12451  pcdvdsb  12489  dvdsprmpweqle  12506  pcfaclem  12518  isstructr  12693  setsvala  12709  setsresg  12716  strle3g  12786  imasaddvallemg  12958  fvprif  12986  mgmsscl  13004  insubm  13117  dfgrp3mlem  13230  mulgdirlem  13283  mulgp1  13285  mulgmodid  13291  eqglact  13355  rngdi  13496  rngdir  13497  rmodislmodlem  13906  rmodislmod  13907  lssclg  13920  2idlcpblrng  14079  qusmulrng  14088  clsss  14354  ntrcls0  14367  neiss  14386  neipsm  14390  cnpnei  14455  cncnp2m  14467  cnconst2  14469  sslm  14483  upxp  14508  txmetcn  14755  ptolemy  15060  sincosq1eq  15075  rplogbval  15181  rpcxplogb  15200  lgsdirprm  15275  lgsdirnn0  15288  gausslemma2dlem1a  15299  gausslemma2dlem3  15304  2lgslem1a1  15327  2lgsoddprmlem1  15346  2lgsoddprmlem2  15347  findset  15591