Theorem 3ad2ant3 1015

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 275	. 2 |- ( ( th /\ ph ) -> ch )
3	2	3adant1 1010	1 |- ( ( ps /\ th /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 973

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

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  simp3l  1020  simp3r  1021  simp31  1028  simp32  1029  simp33  1030  simp3ll  1063  simp3lr  1064  simp3rl  1065  simp3rr  1066  simp3l1  1097  simp3l2  1098  simp3l3  1099  simp3r1  1100  simp3r2  1101  simp3r3  1102  simp31l  1115  simp31r  1116  simp32l  1117  simp32r  1118  simp33l  1119  simp33r  1120  simp311  1139  simp312  1140  simp313  1141  simp321  1142  simp322  1143  simp323  1144  simp331  1145  simp332  1146  simp333  1147  3anim123i  1179  3jaao  1303  ceqsalt  2756  ceqsralt  2757  vtoclgft  2780  ifbothdc  3558  tpssi  3746  sotricim  4308  elirr  4525  en2lp  4538  reg3exmidlemwe  4563  sotri2  5008  poltletr  5011  funprg  5248  funtpg  5249  fntpg  5254  funimaexglem  5281  fvun1  5562  ftpg  5680  fsnunf  5696  fsnunfv  5697  caovimo  6046  brtposg  6233  smoel  6279  rdgivallem  6360  frecsuclem  6385  mapxpen  6826  unsnfi  6896  unsnfidcex  6897  unsnfidcel  6898  sbthlemi4  6937  elfir  6950  updjud  7059  ltsopi  7282  distrnqg  7349  ltmnqg  7363  mulcanenq0ec  7407  distrnq0  7421  prarloclem5  7462  1idprl  7552  1idpru  7553  ltaprg  7581  recexprlemopl  7587  recexprlemopu  7589  recexprlem1ssl  7595  aptipr  7603  ltmprr  7604  cauappcvgprlemlol  7609  cauappcvgprlemupu  7611  caucvgprlemlol  7632  caucvgprlemupu  7634  caucvgprprlemlol  7660  caucvgprprlemupu  7662  readdcan  8059  cnegexlem2  8095  addcan2  8100  ltadd2  8338  apreap  8506  ltmul1  8511  apcotr  8526  apadd1  8527  mulext1  8531  divdirap  8614  divcanap5  8631  ltdiv1  8784  lt2halves  9113  zdivmul  9302  eluzsub  9516  ledivge1le  9683  addlelt  9725  xaddass  9826  xleadd1  9832  xltadd1  9833  elioo5  9890  iccsupr  9923  iccneg  9946  icoshft  9947  icoshftf1o  9948  zltaddlt1le  9964  fzen  9999  elfz1b  10046  fzrevral  10061  fzshftral  10064  elfz0ubfz0  10081  elfz0fzfz0  10082  fz0fzelfz0  10083  fz0fzdiffz0  10086  elfzo  10105  fzodcel  10108  elfzonlteqm1  10166  modqaddmulmod  10347  expdivap  10527  leexp2a  10529  bcval3  10685  omgadd  10737  shftfibg  10784  elicc4abs  11058  xrmaxltsup  11221  xrmaxadd  11224  xrlemininf  11234  xrminltinf  11235  mulcn2  11275  fsumsplitsnun  11382  prodfrecap  11509  demoivreALT  11736  dvdsval2  11752  dvdsmodexp  11757  dvdsmulcr  11783  modmulconst  11785  dvdsexp  11821  oddge22np1  11840  modremain  11888  mulgcd  11971  mulgcdr  11973  gcddiv  11974  rpmulgcd  11981  rplpwr  11982  coprmdvds  12046  cncongr1  12057  dvdsnprmd  12079  prmexpb  12105  rpexp  12107  cncongrprm  12111  modprm0  12208  modprmn0modprm0  12210  coprimeprodsq  12211  pythagtriplem1  12219  pythagtriplem3  12221  pythagtriplem10  12223  pythagtriplem6  12224  pythagtriplem11  12228  pythagtriplem12  12229  pythagtriplem13  12230  pythagtriplem15  12232  pythagtriplem17  12234  pythagtriplem19  12236  pcdvdsb  12273  dvdsprmpweqle  12290  pcfaclem  12301  isstructr  12431  setsvala  12447  setsresg  12454  strle3g  12510  mgmsscl  12615  insubm  12703  clsss  12912  ntrcls0  12925  neiss  12944  neipsm  12948  cnpnei  13013  cncnp2m  13025  cnconst2  13027  sslm  13041  upxp  13066  txmetcn  13313  ptolemy  13539  sincosq1eq  13554  rplogbval  13657  rpcxplogb  13676  lgsdirprm  13729  lgsdirnn0  13742  findset  13980