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  2786  ceqsralt  2787  vtoclgft  2810  ifbothdc  3590  ifnebibdc  3600  tpssi  3785  sotricim  4354  elirr  4573  en2lp  4586  reg3exmidlemwe  4611  sotri2  5063  poltletr  5066  funprg  5304  funtpg  5305  fntpg  5310  funimaexglem  5337  fvun1  5623  ftpg  5742  fsnunf  5758  fsnunfv  5759  caovimo  6112  brtposg  6307  smoel  6353  rdgivallem  6434  frecsuclem  6459  mapxpen  6904  unsnfi  6975  unsnfidcex  6976  unsnfidcel  6977  sbthlemi4  7019  elfir  7032  updjud  7141  ltsopi  7380  distrnqg  7447  ltmnqg  7461  mulcanenq0ec  7505  distrnq0  7519  prarloclem5  7560  1idprl  7650  1idpru  7651  ltaprg  7679  recexprlemopl  7685  recexprlemopu  7687  recexprlem1ssl  7693  aptipr  7701  ltmprr  7702  cauappcvgprlemlol  7707  cauappcvgprlemupu  7709  caucvgprlemlol  7730  caucvgprlemupu  7732  caucvgprprlemlol  7758  caucvgprprlemupu  7760  readdcan  8159  cnegexlem2  8195  addcan2  8200  ltadd2  8438  apreap  8606  ltmul1  8611  apcotr  8626  apadd1  8627  mulext1  8631  divdirap  8716  divcanap5  8733  ltdiv1  8887  lt2halves  9218  zdivmul  9407  eluzsub  9622  ledivge1le  9792  addlelt  9834  xaddass  9935  xleadd1  9941  xltadd1  9942  elioo5  9999  iccsupr  10032  iccneg  10055  icoshft  10056  icoshftf1o  10057  zltaddlt1le  10073  fzen  10109  elfz1b  10156  fzrevral  10171  fzshftral  10174  elfz0ubfz0  10191  elfz0fzfz0  10192  fz0fzelfz0  10193  fz0fzdiffz0  10196  elfzo  10215  fzodcel  10219  elfzonlteqm1  10277  modqaddmulmod  10462  expdivap  10661  leexp2a  10663  bcval3  10822  omgadd  10873  shftfibg  10964  elicc4abs  11238  xrmaxltsup  11401  xrmaxadd  11404  xrlemininf  11414  xrminltinf  11415  mulcn2  11455  fsumsplitsnun  11562  prodfrecap  11689  demoivreALT  11917  dvdsval2  11933  dvdsmodexp  11938  dvdsmulcr  11964  modmulconst  11966  dvdsexp  12003  oddge22np1  12022  modremain  12070  mulgcd  12153  mulgcdr  12155  gcddiv  12156  rpmulgcd  12163  rplpwr  12164  coprmdvds  12230  cncongr1  12241  dvdsnprmd  12263  prmexpb  12289  rpexp  12291  cncongrprm  12295  modprm0  12392  modprmn0modprm0  12394  coprimeprodsq  12395  pythagtriplem1  12403  pythagtriplem3  12405  pythagtriplem10  12407  pythagtriplem6  12408  pythagtriplem11  12412  pythagtriplem12  12413  pythagtriplem13  12414  pythagtriplem15  12416  pythagtriplem17  12418  pythagtriplem19  12420  pcdvdsb  12458  dvdsprmpweqle  12475  pcfaclem  12487  isstructr  12633  setsvala  12649  setsresg  12656  strle3g  12726  imasaddvallemg  12898  fvprif  12926  mgmsscl  12944  insubm  13057  dfgrp3mlem  13170  mulgdirlem  13223  mulgp1  13225  mulgmodid  13231  eqglact  13295  rngdi  13436  rngdir  13437  rmodislmodlem  13846  rmodislmod  13847  lssclg  13860  2idlcpblrng  14019  qusmulrng  14028  clsss  14286  ntrcls0  14299  neiss  14318  neipsm  14322  cnpnei  14387  cncnp2m  14399  cnconst2  14401  sslm  14415  upxp  14440  txmetcn  14687  ptolemy  14959  sincosq1eq  14974  rplogbval  15077  rpcxplogb  15096  lgsdirprm  15150  lgsdirnn0  15163  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  2lgsoddprmlem1  15193  2lgsoddprmlem2  15194  findset  15437