Theorem 3ad2ant3 1044

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 1039	1 |- ( ( ps /\ th /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simp3l  1049  simp3r  1050  simp31  1057  simp32  1058  simp33  1059  simp3ll  1092  simp3lr  1093  simp3rl  1094  simp3rr  1095  simp3l1  1126  simp3l2  1127  simp3l3  1128  simp3r1  1129  simp3r2  1130  simp3r3  1131  simp31l  1144  simp31r  1145  simp32l  1146  simp32r  1147  simp33l  1148  simp33r  1149  simp311  1168  simp312  1169  simp313  1170  simp321  1171  simp322  1172  simp323  1173  simp331  1174  simp332  1175  simp333  1176  3anim123i  1208  3jaao  1342  ceqsalt  2826  ceqsralt  2827  vtoclgft  2851  ifbothdc  3637  ifnebibdc  3648  ssprsseq  3830  tpssi  3837  sotricim  4414  elirr  4633  en2lp  4646  reg3exmidlemwe  4671  sotri2  5126  poltletr  5129  funprg  5371  funtpg  5372  fntpg  5377  funimaexglem  5404  fvun1  5702  ftpg  5827  fsnunf  5843  fsnunfv  5844  caovimo  6205  brtposg  6406  smoel  6452  rdgivallem  6533  frecsuclem  6558  domssr  6937  mapxpen  7017  unsnfi  7092  unsnfidcex  7093  unsnfidcel  7094  sbthlemi4  7138  elfir  7151  updjud  7260  ltsopi  7518  distrnqg  7585  ltmnqg  7599  mulcanenq0ec  7643  distrnq0  7657  prarloclem5  7698  1idprl  7788  1idpru  7789  ltaprg  7817  recexprlemopl  7823  recexprlemopu  7825  recexprlem1ssl  7831  aptipr  7839  ltmprr  7840  cauappcvgprlemlol  7845  cauappcvgprlemupu  7847  caucvgprlemlol  7868  caucvgprlemupu  7870  caucvgprprlemlol  7896  caucvgprprlemupu  7898  readdcan  8297  cnegexlem2  8333  addcan2  8338  ltadd2  8577  apreap  8745  ltmul1  8750  apcotr  8765  apadd1  8766  mulext1  8770  divdirap  8855  divcanap5  8872  ltdiv1  9026  lt2halves  9358  zdivmul  9548  eluzsub  9764  ledivge1le  9934  addlelt  9976  xaddass  10077  xleadd1  10083  xltadd1  10084  elioo5  10141  iccsupr  10174  iccneg  10197  icoshft  10198  icoshftf1o  10199  zltaddlt1le  10215  fzen  10251  elfz1b  10298  fzrevral  10313  fzshftral  10316  elfz0ubfz0  10333  elfz0fzfz0  10334  fz0fzelfz0  10335  fz0fzdiffz0  10338  elfzo  10357  fzodcel  10361  elfzonlteqm1  10428  modqaddmulmod  10625  expdivap  10824  leexp2a  10826  bcval3  10985  omgadd  11036  ccatval1  11145  ccatval2  11146  ccatval3  11147  ccatass  11156  ccats1val2  11187  swrdval2  11199  swrdlen  11200  pfxfv  11232  pfxnd  11237  pfxsuffeqwrdeq  11246  swrdswrdlem  11252  swrdswrd  11253  pfxswrd  11254  pfxpfx  11256  ccats1pfxeq  11262  ccats1pfxeqrex  11263  pfxccatin12lem2  11279  pfxccatpfx1  11284  swrdccat3b  11288  pfxccatid  11289  shftfibg  11347  elicc4abs  11621  xrmaxltsup  11785  xrmaxadd  11788  xrlemininf  11798  xrminltinf  11799  mulcn2  11839  fsumsplitsnun  11946  prodfrecap  12073  demoivreALT  12301  dvdsval2  12317  dvdsmodexp  12322  dvdsmulcr  12348  modmulconst  12350  dvdsexp  12388  oddge22np1  12408  modremain  12456  mulgcd  12553  mulgcdr  12555  gcddiv  12556  rpmulgcd  12563  rplpwr  12564  coprmdvds  12630  cncongr1  12641  dvdsnprmd  12663  prmexpb  12689  rpexp  12691  cncongrprm  12695  modprm0  12793  modprmn0modprm0  12795  coprimeprodsq  12796  pythagtriplem1  12804  pythagtriplem3  12806  pythagtriplem10  12808  pythagtriplem6  12809  pythagtriplem11  12813  pythagtriplem12  12814  pythagtriplem13  12815  pythagtriplem15  12817  pythagtriplem17  12819  pythagtriplem19  12821  pcdvdsb  12859  dvdsprmpweqle  12876  pcfaclem  12888  isstructr  13063  setsvala  13079  setsresg  13086  strle3g  13157  imasaddvallemg  13364  fvprif  13392  mgmsscl  13410  insubm  13534  dfgrp3mlem  13647  mulgdirlem  13706  mulgp1  13708  mulgmodid  13714  eqglact  13778  rngdi  13919  rngdir  13920  rmodislmodlem  14330  rmodislmod  14331  lssclg  14344  2idlcpblrng  14503  qusmulrng  14512  clsss  14808  ntrcls0  14821  neiss  14840  neipsm  14844  cnpnei  14909  cncnp2m  14921  cnconst2  14923  sslm  14937  upxp  14962  txmetcn  15209  ptolemy  15514  sincosq1eq  15529  rplogbval  15635  rpcxplogb  15654  lgsdirprm  15729  lgsdirnn0  15742  gausslemma2dlem1a  15753  gausslemma2dlem3  15758  2lgslem1a1  15781  2lgsoddprmlem1  15800  2lgsoddprmlem2  15801  structiedg0val  15857  lpvtx  15895  incistruhgr  15906  upgredg2vtx  15962  upgredgpr  15963  ausgrumgrien  15984  ausgrusgrien  15985  ushgredgedg  16040  ushgredgedgloop  16042  wlkvtxeledgg  16090  wlkeq  16100  wlkl1loop  16104  uspgr2wlkeq  16111  uspgr2wlkeq2  16112  wlkres  16123  loopclwwlkn1b  16161  clwwlkext2edg  16164  findset  16391