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  2786  vtoclgft  2811  vtoclegft  2833  ifbothdc  3591  ifnebibdc  3601  frirrg  4382  elirr  4574  en2lp  4587  reg3exmidlemwe  4612  sotri3  5065  funtpg  5306  fnprg  5310  fntpg  5311  funimaexglem  5338  fnco  5363  fvun1  5624  oprssov  6062  caovimo  6114  rdgivallem  6436  fnsnsplitdc  6560  funresdfunsndc  6561  f1dom2g  6812  mapxpen  6906  ssfidc  6993  sbthlemi4  7021  ordiso2  7096  updjud  7143  difinfsn  7161  mkvprop  7219  endjudisj  7272  distrnqg  7449  distrnq0  7521  prarloclem5  7562  cauappcvgprlemlol  7709  cauappcvgprlemupu  7711  caucvgprlemlol  7732  caucvgprlemupu  7734  caucvgprprlemlol  7760  caucvgprprlemupu  7762  cnegexlem2  8197  apcotr  8628  apadd1  8629  mulext1  8633  div2negap  8756  ltdiv2  8908  nndivtr  9026  difgtsumgt  9389  zdivmul  9410  gtndiv  9415  fzind  9435  eluzuzle  9603  eluzp1p1  9621  peano2uz  9651  qdivcl  9711  irrmul  9715  ledivge1le  9795  xrre2  9890  xaddass  9938  xltadd1  9945  xlt2add  9949  ubioc1  9998  ubicc2  10054  zltaddlt1le  10076  uzsubsubfz  10116  elfz1b  10159  fzp1nel  10173  fz0fzdiffz0  10199  difelfzle  10203  elfzo0  10252  elfzonlteqm1  10280  fzonn0p1p1  10283  fzosplitprm1  10304  fzoshftral  10308  subfzo0  10312  ceiqle  10387  modqval  10398  modqvalr  10399  flqpmodeq  10401  modq0  10403  mulqmod0  10404  negqmod0  10405  modqge0  10406  modqlt  10407  modqelico  10408  modqdiffl  10409  modqmulnn  10416  modqvalp1  10417  modqmuladdnn0  10442  qnegmod  10443  addmodid  10446  q2submod  10459  modifeq2int  10460  modfzo0difsn  10469  addmodlteq  10472  mulsubdivbinom2ap  10785  omgadd  10876  hashun  10879  redivap  11021  imdivap  11028  xrmaxltsup  11404  xrmaxadd  11407  xrlemininf  11417  xrminltinf  11418  climuni  11439  mulcn2  11458  fsumsplitsnun  11565  prodfap0  11691  fprodabs  11762  efsub  11827  cos12dec  11914  dvdsmodexp  11941  summodnegmod  11968  divalglemex  12066  divalg  12068  modremain  12073  ndvdssub  12074  fldivndvdslt  12079  nndvdslegcd  12105  dfgcd2  12154  mulgcd  12156  mulgcdr  12158  gcddiv  12159  rplpwr  12167  rppwr  12168  qredeq  12237  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  pw2dvdslemn  12306  hashgcdlem  12379  modprm0  12395  modprmn0modprm0  12397  pythagtriplem1  12406  pythagtriplem3  12408  pythagtriplem10  12410  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem11  12415  pythagtriplem12  12416  pythagtriplem13  12417  pythagtriplem14  12418  pythagtriplem19  12423  pythagtrip  12424  dvdsprmpweqnn  12477  difsqpwdvds  12479  pcfaclem  12490  pcbc  12492  unennn  12557  ptex  12878  imasaddvallemg  12901  fvprif  12929  mgmsscl  12947  insubm  13060  mulginvcom  13220  mulgassr  13233  mulgmodid  13234  quselbasg  13303  ghmnsgima  13341  ringrng  13535  rmodislmodlem  13849  rmodislmod  13850  lssincl  13884  sralmod  13949  rnglidlmmgm  13995  rnglidlmsgrp  13996  rnglidlrng  13997  2idlcpblrng  14022  psrbaglesuppg  14169  ntrin  14303  elnei  14331  restco  14353  cnpnei  14398  cncnp2m  14410  sslm  14426  upxp  14451  blres  14613  metcnp3  14690  tgqioo  14734  dvply1  14943  ptolemy  15000  cxpcom  15112  logbgcd1irr  15140  logbprmirr  15145  lgslem1  15157  lgsneg  15181  lgsdilem  15184  lgsdir  15192  lgssq2  15198  lgsdirnn0  15204  gausslemma2dlem1a  15215  2lgslem1a1  15243