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  2803  ceqsralt  2804  vtoclgft  2828  ifbothdc  3614  ifnebibdc  3625  ssprsseq  3806  tpssi  3813  sotricim  4388  elirr  4607  en2lp  4620  reg3exmidlemwe  4645  sotri2  5099  poltletr  5102  funprg  5343  funtpg  5344  fntpg  5349  funimaexglem  5376  fvun1  5668  ftpg  5791  fsnunf  5807  fsnunfv  5808  caovimo  6163  brtposg  6363  smoel  6409  rdgivallem  6490  frecsuclem  6515  domssr  6892  mapxpen  6970  unsnfi  7042  unsnfidcex  7043  unsnfidcel  7044  sbthlemi4  7088  elfir  7101  updjud  7210  ltsopi  7468  distrnqg  7535  ltmnqg  7549  mulcanenq0ec  7593  distrnq0  7607  prarloclem5  7648  1idprl  7738  1idpru  7739  ltaprg  7767  recexprlemopl  7773  recexprlemopu  7775  recexprlem1ssl  7781  aptipr  7789  ltmprr  7790  cauappcvgprlemlol  7795  cauappcvgprlemupu  7797  caucvgprlemlol  7818  caucvgprlemupu  7820  caucvgprprlemlol  7846  caucvgprprlemupu  7848  readdcan  8247  cnegexlem2  8283  addcan2  8288  ltadd2  8527  apreap  8695  ltmul1  8700  apcotr  8715  apadd1  8716  mulext1  8720  divdirap  8805  divcanap5  8822  ltdiv1  8976  lt2halves  9308  zdivmul  9498  eluzsub  9713  ledivge1le  9883  addlelt  9925  xaddass  10026  xleadd1  10032  xltadd1  10033  elioo5  10090  iccsupr  10123  iccneg  10146  icoshft  10147  icoshftf1o  10148  zltaddlt1le  10164  fzen  10200  elfz1b  10247  fzrevral  10262  fzshftral  10265  elfz0ubfz0  10282  elfz0fzfz0  10283  fz0fzelfz0  10284  fz0fzdiffz0  10287  elfzo  10306  fzodcel  10310  elfzonlteqm1  10376  modqaddmulmod  10573  expdivap  10772  leexp2a  10774  bcval3  10933  omgadd  10984  ccatval1  11091  ccatval2  11092  ccatval3  11093  ccatass  11102  ccats1val2  11130  swrdval2  11142  swrdlen  11143  pfxfv  11175  pfxnd  11180  pfxsuffeqwrdeq  11189  swrdswrdlem  11195  swrdswrd  11196  pfxswrd  11197  pfxpfx  11199  ccats1pfxeq  11205  ccats1pfxeqrex  11206  pfxccatin12lem2  11222  pfxccatpfx1  11227  swrdccat3b  11231  pfxccatid  11232  shftfibg  11246  elicc4abs  11520  xrmaxltsup  11684  xrmaxadd  11687  xrlemininf  11697  xrminltinf  11698  mulcn2  11738  fsumsplitsnun  11845  prodfrecap  11972  demoivreALT  12200  dvdsval2  12216  dvdsmodexp  12221  dvdsmulcr  12247  modmulconst  12249  dvdsexp  12287  oddge22np1  12307  modremain  12355  mulgcd  12452  mulgcdr  12454  gcddiv  12455  rpmulgcd  12462  rplpwr  12463  coprmdvds  12529  cncongr1  12540  dvdsnprmd  12562  prmexpb  12588  rpexp  12590  cncongrprm  12594  modprm0  12692  modprmn0modprm0  12694  coprimeprodsq  12695  pythagtriplem1  12703  pythagtriplem3  12705  pythagtriplem10  12707  pythagtriplem6  12708  pythagtriplem11  12712  pythagtriplem12  12713  pythagtriplem13  12714  pythagtriplem15  12716  pythagtriplem17  12718  pythagtriplem19  12720  pcdvdsb  12758  dvdsprmpweqle  12775  pcfaclem  12787  isstructr  12962  setsvala  12978  setsresg  12985  strle3g  13055  imasaddvallemg  13262  fvprif  13290  mgmsscl  13308  insubm  13432  dfgrp3mlem  13545  mulgdirlem  13604  mulgp1  13606  mulgmodid  13612  eqglact  13676  rngdi  13817  rngdir  13818  rmodislmodlem  14227  rmodislmod  14228  lssclg  14241  2idlcpblrng  14400  qusmulrng  14409  clsss  14705  ntrcls0  14718  neiss  14737  neipsm  14741  cnpnei  14806  cncnp2m  14818  cnconst2  14820  sslm  14834  upxp  14859  txmetcn  15106  ptolemy  15411  sincosq1eq  15426  rplogbval  15532  rpcxplogb  15551  lgsdirprm  15626  lgsdirnn0  15639  gausslemma2dlem1a  15650  gausslemma2dlem3  15655  2lgslem1a1  15678  2lgsoddprmlem1  15697  2lgsoddprmlem2  15698  structiedg0val  15754  lpvtx  15790  incistruhgr  15801  upgredg2vtx  15852  upgredgpr  15853  findset  16080