Theorem 3ad2ant2 1021

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	|- ( ph -> ch )

Assertion

Ref	Expression
3ad2ant2	|- ( ( ps /\ ph /\ th ) -> ch )

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant1 1017	1 |- ( ( ps /\ ph /\ th ) -> 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:  simp2l  1025  simp2r  1026  simp21  1032  simp22  1033  simp23  1034  simp2ll  1066  simp2lr  1067  simp2rl  1068  simp2rr  1069  simp2l1  1098  simp2l2  1099  simp2l3  1100  simp2r1  1101  simp2r2  1102  simp2r3  1103  simp21l  1116  simp21r  1117  simp22l  1118  simp22r  1119  simp23l  1120  simp23r  1121  simp211  1137  simp212  1138  simp213  1139  simp221  1140  simp222  1141  simp223  1142  simp231  1143  simp232  1144  simp233  1145  3anim123i  1186  3jaao  1319  ceqsalt  2789  vtoclgft  2814  vtoclegft  2836  ifbothdc  3595  ifnebibdc  3605  frirrg  4386  elirr  4578  en2lp  4591  reg3exmidlemwe  4616  sotri3  5069  funtpg  5310  fnprg  5314  fntpg  5315  funimaexglem  5342  fnco  5369  fvun1  5630  oprssov  6069  caovimo  6121  rdgivallem  6448  fnsnsplitdc  6572  funresdfunsndc  6573  f1dom2g  6824  mapxpen  6918  ssfidc  7007  sbthlemi4  7035  ordiso2  7110  updjud  7157  difinfsn  7175  mkvprop  7233  endjudisj  7293  distrnqg  7471  distrnq0  7543  prarloclem5  7584  cauappcvgprlemlol  7731  cauappcvgprlemupu  7733  caucvgprlemlol  7754  caucvgprlemupu  7756  caucvgprprlemlol  7782  caucvgprprlemupu  7784  cnegexlem2  8219  apcotr  8651  apadd1  8652  mulext1  8656  div2negap  8779  ltdiv2  8931  nndivtr  9049  difgtsumgt  9412  zdivmul  9433  gtndiv  9438  fzind  9458  eluzuzle  9626  eluzp1p1  9644  peano2uz  9674  qdivcl  9734  irrmul  9738  ledivge1le  9818  xrre2  9913  xaddass  9961  xltadd1  9968  xlt2add  9972  ubioc1  10021  ubicc2  10077  zltaddlt1le  10099  uzsubsubfz  10139  elfz1b  10182  fzp1nel  10196  fz0fzdiffz0  10222  difelfzle  10226  elfzo0  10275  elfzonlteqm1  10303  fzonn0p1p1  10306  fzosplitprm1  10327  fzoshftral  10331  subfzo0  10335  ceiqle  10422  modqval  10433  modqvalr  10434  flqpmodeq  10436  modq0  10438  mulqmod0  10439  negqmod0  10440  modqge0  10441  modqlt  10442  modqelico  10443  modqdiffl  10444  modqmulnn  10451  modqvalp1  10452  modqmuladdnn0  10477  qnegmod  10478  addmodid  10481  q2submod  10494  modifeq2int  10495  modfzo0difsn  10504  addmodlteq  10507  mulsubdivbinom2ap  10820  omgadd  10911  hashun  10914  redivap  11056  imdivap  11063  xrmaxltsup  11440  xrmaxadd  11443  xrlemininf  11453  xrminltinf  11454  climuni  11475  mulcn2  11494  fsumsplitsnun  11601  prodfap0  11727  fprodabs  11798  efsub  11863  cos12dec  11950  dvdsmodexp  11977  summodnegmod  12004  divalglemex  12104  divalg  12106  modremain  12111  ndvdssub  12112  fldivndvdslt  12119  bitsfzo  12137  nndvdslegcd  12157  dfgcd2  12206  mulgcd  12208  mulgcdr  12210  gcddiv  12211  rplpwr  12219  rppwr  12220  qredeq  12289  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  pw2dvdslemn  12358  hashgcdlem  12431  modprm0  12448  modprmn0modprm0  12450  pythagtriplem1  12459  pythagtriplem3  12461  pythagtriplem10  12463  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem11  12468  pythagtriplem12  12469  pythagtriplem13  12470  pythagtriplem14  12471  pythagtriplem19  12476  pythagtrip  12477  dvdsprmpweqnn  12530  difsqpwdvds  12532  pcfaclem  12543  pcbc  12545  unennn  12639  ptex  12966  imasaddvallemg  13017  fvprif  13045  mgmsscl  13063  insubm  13187  mulginvcom  13353  mulgassr  13366  mulgmodid  13367  quselbasg  13436  ghmnsgima  13474  ringrng  13668  rmodislmodlem  13982  rmodislmod  13983  lssincl  14017  sralmod  14082  rnglidlmmgm  14128  rnglidlmsgrp  14129  rnglidlrng  14130  2idlcpblrng  14155  psrbaglesuppg  14302  ntrin  14444  elnei  14472  restco  14494  cnpnei  14539  cncnp2m  14551  sslm  14567  upxp  14592  blres  14754  metcnp3  14831  tgqioo  14875  dvply1  15085  ptolemy  15144  cxpcom  15258  logbgcd1irr  15287  logbprmirr  15292  lgslem1  15325  lgsneg  15349  lgsdilem  15352  lgsdir  15360  lgssq2  15366  lgsdirnn0  15372  gausslemma2dlem1a  15383  2lgslem1a1  15411