Theorem 3ad2ant3 1021

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

Syntax hints:   -> wi 4   /\ w3a 979

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 981

This theorem is referenced by:  simp3l  1026  simp3r  1027  simp31  1034  simp32  1035  simp33  1036  simp3ll  1069  simp3lr  1070  simp3rl  1071  simp3rr  1072  simp3l1  1103  simp3l2  1104  simp3l3  1105  simp3r1  1106  simp3r2  1107  simp3r3  1108  simp31l  1121  simp31r  1122  simp32l  1123  simp32r  1124  simp33l  1125  simp33r  1126  simp311  1145  simp312  1146  simp313  1147  simp321  1148  simp322  1149  simp323  1150  simp331  1151  simp332  1152  simp333  1153  3anim123i  1185  3jaao  1318  ceqsalt  2775  ceqsralt  2776  vtoclgft  2799  ifbothdc  3579  tpssi  3771  sotricim  4335  elirr  4552  en2lp  4565  reg3exmidlemwe  4590  sotri2  5038  poltletr  5041  funprg  5278  funtpg  5279  fntpg  5284  funimaexglem  5311  fvun1  5595  ftpg  5713  fsnunf  5729  fsnunfv  5730  caovimo  6082  brtposg  6269  smoel  6315  rdgivallem  6396  frecsuclem  6421  mapxpen  6862  unsnfi  6932  unsnfidcex  6933  unsnfidcel  6934  sbthlemi4  6973  elfir  6986  updjud  7095  ltsopi  7333  distrnqg  7400  ltmnqg  7414  mulcanenq0ec  7458  distrnq0  7472  prarloclem5  7513  1idprl  7603  1idpru  7604  ltaprg  7632  recexprlemopl  7638  recexprlemopu  7640  recexprlem1ssl  7646  aptipr  7654  ltmprr  7655  cauappcvgprlemlol  7660  cauappcvgprlemupu  7662  caucvgprlemlol  7683  caucvgprlemupu  7685  caucvgprprlemlol  7711  caucvgprprlemupu  7713  readdcan  8111  cnegexlem2  8147  addcan2  8152  ltadd2  8390  apreap  8558  ltmul1  8563  apcotr  8578  apadd1  8579  mulext1  8583  divdirap  8668  divcanap5  8685  ltdiv1  8839  lt2halves  9168  zdivmul  9357  eluzsub  9571  ledivge1le  9740  addlelt  9782  xaddass  9883  xleadd1  9889  xltadd1  9890  elioo5  9947  iccsupr  9980  iccneg  10003  icoshft  10004  icoshftf1o  10005  zltaddlt1le  10021  fzen  10057  elfz1b  10104  fzrevral  10119  fzshftral  10122  elfz0ubfz0  10139  elfz0fzfz0  10140  fz0fzelfz0  10141  fz0fzdiffz0  10144  elfzo  10163  fzodcel  10166  elfzonlteqm1  10224  modqaddmulmod  10405  expdivap  10585  leexp2a  10587  bcval3  10745  omgadd  10796  shftfibg  10843  elicc4abs  11117  xrmaxltsup  11280  xrmaxadd  11283  xrlemininf  11293  xrminltinf  11294  mulcn2  11334  fsumsplitsnun  11441  prodfrecap  11568  demoivreALT  11795  dvdsval2  11811  dvdsmodexp  11816  dvdsmulcr  11842  modmulconst  11844  dvdsexp  11881  oddge22np1  11900  modremain  11948  mulgcd  12031  mulgcdr  12033  gcddiv  12034  rpmulgcd  12041  rplpwr  12042  coprmdvds  12106  cncongr1  12117  dvdsnprmd  12139  prmexpb  12165  rpexp  12167  cncongrprm  12171  modprm0  12268  modprmn0modprm0  12270  coprimeprodsq  12271  pythagtriplem1  12279  pythagtriplem3  12281  pythagtriplem10  12283  pythagtriplem6  12284  pythagtriplem11  12288  pythagtriplem12  12289  pythagtriplem13  12290  pythagtriplem15  12292  pythagtriplem17  12294  pythagtriplem19  12296  pcdvdsb  12333  dvdsprmpweqle  12350  pcfaclem  12361  isstructr  12491  setsvala  12507  setsresg  12514  strle3g  12582  imasaddvallemg  12754  fvprif  12781  mgmsscl  12799  insubm  12894  dfgrp3mlem  12995  mulgdirlem  13046  mulgp1  13048  mulgmodid  13054  eqglact  13117  rngdi  13192  rngdir  13193  rmodislmodlem  13539  rmodislmod  13540  lssclg  13553  2idlcpblrng  13711  qusmulrng  13719  clsss  13914  ntrcls0  13927  neiss  13946  neipsm  13950  cnpnei  14015  cncnp2m  14027  cnconst2  14029  sslm  14043  upxp  14068  txmetcn  14315  ptolemy  14541  sincosq1eq  14556  rplogbval  14659  rpcxplogb  14678  lgsdirprm  14731  lgsdirnn0  14744  2lgsoddprmlem1  14749  2lgsoddprmlem2  14750  findset  14993