Theorem 3ad2ant3 1020

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  simp3l  1025  simp3r  1026  simp31  1033  simp32  1034  simp33  1035  simp3ll  1068  simp3lr  1069  simp3rl  1070  simp3rr  1071  simp3l1  1102  simp3l2  1103  simp3l3  1104  simp3r1  1105  simp3r2  1106  simp3r3  1107  simp31l  1120  simp31r  1121  simp32l  1122  simp32r  1123  simp33l  1124  simp33r  1125  simp311  1144  simp312  1145  simp313  1146  simp321  1147  simp322  1148  simp323  1149  simp331  1150  simp332  1151  simp333  1152  3anim123i  1184  3jaao  1308  ceqsalt  2765  ceqsralt  2766  vtoclgft  2789  ifbothdc  3569  tpssi  3761  sotricim  4325  elirr  4542  en2lp  4555  reg3exmidlemwe  4580  sotri2  5028  poltletr  5031  funprg  5268  funtpg  5269  fntpg  5274  funimaexglem  5301  fvun1  5584  ftpg  5702  fsnunf  5718  fsnunfv  5719  caovimo  6070  brtposg  6257  smoel  6303  rdgivallem  6384  frecsuclem  6409  mapxpen  6850  unsnfi  6920  unsnfidcex  6921  unsnfidcel  6922  sbthlemi4  6961  elfir  6974  updjud  7083  ltsopi  7321  distrnqg  7388  ltmnqg  7402  mulcanenq0ec  7446  distrnq0  7460  prarloclem5  7501  1idprl  7591  1idpru  7592  ltaprg  7620  recexprlemopl  7626  recexprlemopu  7628  recexprlem1ssl  7634  aptipr  7642  ltmprr  7643  cauappcvgprlemlol  7648  cauappcvgprlemupu  7650  caucvgprlemlol  7671  caucvgprlemupu  7673  caucvgprprlemlol  7699  caucvgprprlemupu  7701  readdcan  8099  cnegexlem2  8135  addcan2  8140  ltadd2  8378  apreap  8546  ltmul1  8551  apcotr  8566  apadd1  8567  mulext1  8571  divdirap  8656  divcanap5  8673  ltdiv1  8827  lt2halves  9156  zdivmul  9345  eluzsub  9559  ledivge1le  9728  addlelt  9770  xaddass  9871  xleadd1  9877  xltadd1  9878  elioo5  9935  iccsupr  9968  iccneg  9991  icoshft  9992  icoshftf1o  9993  zltaddlt1le  10009  fzen  10045  elfz1b  10092  fzrevral  10107  fzshftral  10110  elfz0ubfz0  10127  elfz0fzfz0  10128  fz0fzelfz0  10129  fz0fzdiffz0  10132  elfzo  10151  fzodcel  10154  elfzonlteqm1  10212  modqaddmulmod  10393  expdivap  10573  leexp2a  10575  bcval3  10733  omgadd  10784  shftfibg  10831  elicc4abs  11105  xrmaxltsup  11268  xrmaxadd  11271  xrlemininf  11281  xrminltinf  11282  mulcn2  11322  fsumsplitsnun  11429  prodfrecap  11556  demoivreALT  11783  dvdsval2  11799  dvdsmodexp  11804  dvdsmulcr  11830  modmulconst  11832  dvdsexp  11869  oddge22np1  11888  modremain  11936  mulgcd  12019  mulgcdr  12021  gcddiv  12022  rpmulgcd  12029  rplpwr  12030  coprmdvds  12094  cncongr1  12105  dvdsnprmd  12127  prmexpb  12153  rpexp  12155  cncongrprm  12159  modprm0  12256  modprmn0modprm0  12258  coprimeprodsq  12259  pythagtriplem1  12267  pythagtriplem3  12269  pythagtriplem10  12271  pythagtriplem6  12272  pythagtriplem11  12276  pythagtriplem12  12277  pythagtriplem13  12278  pythagtriplem15  12280  pythagtriplem17  12282  pythagtriplem19  12284  pcdvdsb  12321  dvdsprmpweqle  12338  pcfaclem  12349  isstructr  12479  setsvala  12495  setsresg  12502  strle3g  12569  imasaddvallemg  12741  fvprif  12767  mgmsscl  12785  insubm  12877  dfgrp3mlem  12973  mulgdirlem  13019  mulgp1  13021  mulgmodid  13027  eqglact  13089  rmodislmodlem  13445  rmodislmod  13446  lssclg  13456  clsss  13657  ntrcls0  13670  neiss  13689  neipsm  13693  cnpnei  13758  cncnp2m  13770  cnconst2  13772  sslm  13786  upxp  13811  txmetcn  14058  ptolemy  14284  sincosq1eq  14299  rplogbval  14402  rpcxplogb  14421  lgsdirprm  14474  lgsdirnn0  14487  2lgsoddprmlem1  14492  2lgsoddprmlem2  14493  findset  14736