Theorem 3ad2ant3 1023

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  simp3l  1028  simp3r  1029  simp31  1036  simp32  1037  simp33  1038  simp3ll  1071  simp3lr  1072  simp3rl  1073  simp3rr  1074  simp3l1  1105  simp3l2  1106  simp3l3  1107  simp3r1  1108  simp3r2  1109  simp3r3  1110  simp31l  1123  simp31r  1124  simp32l  1125  simp32r  1126  simp33l  1127  simp33r  1128  simp311  1147  simp312  1148  simp313  1149  simp321  1150  simp322  1151  simp323  1152  simp331  1153  simp332  1154  simp333  1155  3anim123i  1187  3jaao  1321  ceqsalt  2798  ceqsralt  2799  vtoclgft  2823  ifbothdc  3605  ifnebibdc  3615  tpssi  3800  sotricim  4371  elirr  4590  en2lp  4603  reg3exmidlemwe  4628  sotri2  5081  poltletr  5084  funprg  5325  funtpg  5326  fntpg  5331  funimaexglem  5358  fvun1  5647  ftpg  5770  fsnunf  5786  fsnunfv  5787  caovimo  6142  brtposg  6342  smoel  6388  rdgivallem  6469  frecsuclem  6494  domssr  6871  mapxpen  6947  unsnfi  7018  unsnfidcex  7019  unsnfidcel  7020  sbthlemi4  7064  elfir  7077  updjud  7186  ltsopi  7435  distrnqg  7502  ltmnqg  7516  mulcanenq0ec  7560  distrnq0  7574  prarloclem5  7615  1idprl  7705  1idpru  7706  ltaprg  7734  recexprlemopl  7740  recexprlemopu  7742  recexprlem1ssl  7748  aptipr  7756  ltmprr  7757  cauappcvgprlemlol  7762  cauappcvgprlemupu  7764  caucvgprlemlol  7785  caucvgprlemupu  7787  caucvgprprlemlol  7813  caucvgprprlemupu  7815  readdcan  8214  cnegexlem2  8250  addcan2  8255  ltadd2  8494  apreap  8662  ltmul1  8667  apcotr  8682  apadd1  8683  mulext1  8687  divdirap  8772  divcanap5  8789  ltdiv1  8943  lt2halves  9275  zdivmul  9465  eluzsub  9680  ledivge1le  9850  addlelt  9892  xaddass  9993  xleadd1  9999  xltadd1  10000  elioo5  10057  iccsupr  10090  iccneg  10113  icoshft  10114  icoshftf1o  10115  zltaddlt1le  10131  fzen  10167  elfz1b  10214  fzrevral  10229  fzshftral  10232  elfz0ubfz0  10249  elfz0fzfz0  10250  fz0fzelfz0  10251  fz0fzdiffz0  10254  elfzo  10273  fzodcel  10277  elfzonlteqm1  10341  modqaddmulmod  10538  expdivap  10737  leexp2a  10739  bcval3  10898  omgadd  10949  ccatval1  11056  ccatval2  11057  ccatval3  11058  ccatass  11067  ccats1val2  11095  swrdval2  11107  swrdlen  11108  pfxfv  11138  pfxnd  11143  pfxsuffeqwrdeq  11152  shftfibg  11164  elicc4abs  11438  xrmaxltsup  11602  xrmaxadd  11605  xrlemininf  11615  xrminltinf  11616  mulcn2  11656  fsumsplitsnun  11763  prodfrecap  11890  demoivreALT  12118  dvdsval2  12134  dvdsmodexp  12139  dvdsmulcr  12165  modmulconst  12167  dvdsexp  12205  oddge22np1  12225  modremain  12273  mulgcd  12370  mulgcdr  12372  gcddiv  12373  rpmulgcd  12380  rplpwr  12381  coprmdvds  12447  cncongr1  12458  dvdsnprmd  12480  prmexpb  12506  rpexp  12508  cncongrprm  12512  modprm0  12610  modprmn0modprm0  12612  coprimeprodsq  12613  pythagtriplem1  12621  pythagtriplem3  12623  pythagtriplem10  12625  pythagtriplem6  12626  pythagtriplem11  12630  pythagtriplem12  12631  pythagtriplem13  12632  pythagtriplem15  12634  pythagtriplem17  12636  pythagtriplem19  12638  pcdvdsb  12676  dvdsprmpweqle  12693  pcfaclem  12705  isstructr  12880  setsvala  12896  setsresg  12903  strle3g  12973  imasaddvallemg  13180  fvprif  13208  mgmsscl  13226  insubm  13350  dfgrp3mlem  13463  mulgdirlem  13522  mulgp1  13524  mulgmodid  13530  eqglact  13594  rngdi  13735  rngdir  13736  rmodislmodlem  14145  rmodislmod  14146  lssclg  14159  2idlcpblrng  14318  qusmulrng  14327  clsss  14623  ntrcls0  14636  neiss  14655  neipsm  14659  cnpnei  14724  cncnp2m  14736  cnconst2  14738  sslm  14752  upxp  14777  txmetcn  15024  ptolemy  15329  sincosq1eq  15344  rplogbval  15450  rpcxplogb  15469  lgsdirprm  15544  lgsdirnn0  15557  gausslemma2dlem1a  15568  gausslemma2dlem3  15573  2lgslem1a1  15596  2lgsoddprmlem1  15615  2lgsoddprmlem2  15616  structiedg0val  15670  findset  15918