Theorem 3ad2ant3 1047

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simp3l  1052  simp3r  1053  simp31  1060  simp32  1061  simp33  1062  simp3ll  1095  simp3lr  1096  simp3rl  1097  simp3rr  1098  simp3l1  1129  simp3l2  1130  simp3l3  1131  simp3r1  1132  simp3r2  1133  simp3r3  1134  simp31l  1147  simp31r  1148  simp32l  1149  simp32r  1150  simp33l  1151  simp33r  1152  simp311  1171  simp312  1172  simp313  1173  simp321  1174  simp322  1175  simp323  1176  simp331  1177  simp332  1178  simp333  1179  3anim123i  1211  3jaao  1345  ceqsalt  2842  ceqsralt  2843  vtoclgft  2867  ifbothdc  3659  ifnebibdc  3670  ssprsseq  3858  tpssi  3865  sotricim  4446  elirr  4665  en2lp  4678  reg3exmidlemwe  4703  sotri2  5162  poltletr  5165  funprg  5408  funtpg  5409  fntpg  5414  funimaexglem  5441  fvun1  5745  ftpg  5870  fsnunf  5886  fsnunfv  5887  caovimo  6250  funsssuppss  6460  brtposg  6487  smoel  6533  rdgivallem  6614  frecsuclem  6639  domssr  7019  mapxpen  7103  unsnfi  7181  unsnfidcex  7182  unsnfidcel  7183  sbthlemi4  7232  elfir  7262  updjud  7375  ltsopi  7637  distrnqg  7704  ltmnqg  7718  mulcanenq0ec  7762  distrnq0  7776  prarloclem5  7817  1idprl  7907  1idpru  7908  ltaprg  7936  recexprlemopl  7942  recexprlemopu  7944  recexprlem1ssl  7950  aptipr  7958  ltmprr  7959  cauappcvgprlemlol  7964  cauappcvgprlemupu  7966  caucvgprlemlol  7987  caucvgprlemupu  7989  caucvgprprlemlol  8015  caucvgprprlemupu  8017  readdcan  8415  cnegexlem2  8451  addcan2  8456  ltadd2  8695  apreap  8863  ltmul1  8868  apcotr  8883  apadd1  8884  mulext1  8888  divdirap  8973  divcanap5  8990  ltdiv1  9144  lt2halves  9476  zdivmul  9671  eluzsub  9887  ledivge1le  10062  addlelt  10104  xaddass  10205  xleadd1  10211  xltadd1  10212  elioo5  10269  iccsupr  10302  iccneg  10325  icoshft  10326  icoshftf1o  10327  zltaddlt1le  10344  fzen  10380  elfz1b  10428  fzrevral  10443  fzshftral  10446  elfz0ubfz0  10463  elfz0fzfz0  10464  fz0fzelfz0  10465  fz0fzdiffz0  10468  elfzo  10487  fzodcel  10491  elfzonlteqm1  10559  modqaddmulmod  10757  expdivap  10956  leexp2a  10958  bcval3  11117  omgadd  11170  ccatval1  11289  ccatval2  11290  ccatval3  11291  ccatass  11300  ccats1val2  11332  swrdval2  11347  swrdlen  11348  pfxfv  11380  pfxnd  11385  pfxsuffeqwrdeq  11394  swrdswrdlem  11400  swrdswrd  11401  pfxswrd  11402  pfxpfx  11404  ccats1pfxeq  11410  ccats1pfxeqrex  11411  pfxccatin12lem2  11427  pfxccatpfx1  11432  swrdccat3b  11436  pfxccatid  11437  shftfibg  11509  elicc4abs  11783  xrmaxltsup  11947  xrmaxadd  11950  xrlemininf  11960  xrminltinf  11961  mulcn2  12001  fsumsplitsnun  12109  prodfrecap  12236  demoivreALT  12464  dvdsval2  12480  dvdsmodexp  12485  dvdsmulcr  12511  modmulconst  12513  dvdsexp  12551  oddge22np1  12571  modremain  12619  mulgcd  12716  mulgcdr  12718  gcddiv  12719  rpmulgcd  12726  rplpwr  12727  coprmdvds  12793  cncongr1  12804  dvdsnprmd  12826  prmexpb  12852  rpexp  12854  cncongrprm  12858  modprm0  12956  modprmn0modprm0  12958  coprimeprodsq  12959  pythagtriplem1  12967  pythagtriplem3  12969  pythagtriplem10  12971  pythagtriplem6  12972  pythagtriplem11  12976  pythagtriplem12  12977  pythagtriplem13  12978  pythagtriplem15  12980  pythagtriplem17  12982  pythagtriplem19  12984  pcdvdsb  13022  dvdsprmpweqle  13039  pcfaclem  13051  isstructr  13244  setsvala  13260  setsresg  13267  strle3g  13338  imasaddvallemg  13545  fvprif  13573  mgmsscl  13591  insubm  13715  dfgrp3mlem  13828  mulgdirlem  13887  mulgp1  13889  mulgmodid  13895  eqglact  13959  rngdi  14101  rngdir  14102  rmodislmodlem  14515  rmodislmod  14516  lssclg  14529  2idlcpblrng  14688  qusmulrng  14697  psrbagaddclfi  14842  clsss  15000  ntrcls0  15013  neiss  15032  neipsm  15036  cnpnei  15101  cncnp2m  15113  cnconst2  15115  sslm  15129  upxp  15154  txmetcn  15401  ptolemy  15706  sincosq1eq  15721  rplogbval  15827  rpcxplogb  15846  pellexlem1  15862  lgsdirprm  15924  lgsdirnn0  15937  gausslemma2dlem1a  15948  gausslemma2dlem3  15953  2lgslem1a1  15976  2lgsoddprmlem1  15995  2lgsoddprmlem2  15996  structiedg0val  16052  lpvtx  16091  incistruhgr  16102  upgredg2vtx  16160  upgredgpr  16161  ausgrumgrien  16182  ausgrusgrien  16183  ushgredgedg  16238  ushgredgedgloop  16240  uhgrissubgr  16273  egrsubgr  16275  0uhgrsubgr  16277  wlkvtxeledgg  16356  wlkeq  16366  wlkl1loop  16370  uspgr2wlkeq  16377  uspgr2wlkeq2  16378  wlkres  16391  loopclwwlkn1b  16431  clwwlkext2edg  16434  clwwlknonex2lem2  16450  clwwlknonex2  16451  clwwlknun  16453  eupth2lem3lem6fi  16483  findset  16732