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  2778  vtoclgft  2802  vtoclegft  2824  ifbothdc  3582  frirrg  4365  elirr  4555  en2lp  4568  reg3exmidlemwe  4593  sotri3  5042  funtpg  5282  fnprg  5286  fntpg  5287  funimaexglem  5314  fnco  5339  fvun1  5598  oprssov  6033  caovimo  6085  rdgivallem  6400  fnsnsplitdc  6524  funresdfunsndc  6525  f1dom2g  6774  mapxpen  6866  ssfidc  6952  sbthlemi4  6977  ordiso2  7052  updjud  7099  difinfsn  7117  mkvprop  7174  endjudisj  7227  distrnqg  7404  distrnq0  7476  prarloclem5  7517  cauappcvgprlemlol  7664  cauappcvgprlemupu  7666  caucvgprlemlol  7687  caucvgprlemupu  7689  caucvgprprlemlol  7715  caucvgprprlemupu  7717  cnegexlem2  8151  apcotr  8582  apadd1  8583  mulext1  8587  div2negap  8710  ltdiv2  8862  nndivtr  8979  difgtsumgt  9340  zdivmul  9361  gtndiv  9366  fzind  9386  eluzuzle  9554  eluzp1p1  9571  peano2uz  9601  qdivcl  9661  irrmul  9665  ledivge1le  9744  xrre2  9839  xaddass  9887  xltadd1  9894  xlt2add  9898  ubioc1  9947  ubicc2  10003  zltaddlt1le  10025  uzsubsubfz  10065  elfz1b  10108  fzp1nel  10122  fz0fzdiffz0  10148  difelfzle  10152  elfzo0  10200  elfzonlteqm1  10228  fzonn0p1p1  10231  fzosplitprm1  10252  fzoshftral  10256  subfzo0  10260  ceiqle  10331  modqval  10342  modqvalr  10343  flqpmodeq  10345  modq0  10347  mulqmod0  10348  negqmod0  10349  modqge0  10350  modqlt  10351  modqelico  10352  modqdiffl  10353  modqmulnn  10360  modqvalp1  10361  modqmuladdnn0  10386  qnegmod  10387  addmodid  10390  q2submod  10403  modifeq2int  10404  modfzo0difsn  10413  addmodlteq  10416  mulsubdivbinom2ap  10709  omgadd  10800  hashun  10803  redivap  10901  imdivap  10908  xrmaxltsup  11284  xrmaxadd  11287  xrlemininf  11297  xrminltinf  11298  climuni  11319  mulcn2  11338  fsumsplitsnun  11445  prodfap0  11571  fprodabs  11642  efsub  11707  cos12dec  11793  dvdsmodexp  11820  summodnegmod  11847  divalglemex  11945  divalg  11947  modremain  11952  ndvdssub  11953  fldivndvdslt  11958  nndvdslegcd  11984  dfgcd2  12033  mulgcd  12035  mulgcdr  12037  gcddiv  12038  rplpwr  12046  rppwr  12047  qredeq  12114  divgcdcoprmex  12120  cncongr1  12121  cncongr2  12122  pw2dvdslemn  12183  hashgcdlem  12256  modprm0  12272  modprmn0modprm0  12274  pythagtriplem1  12283  pythagtriplem3  12285  pythagtriplem10  12287  pythagtriplem6  12288  pythagtriplem7  12289  pythagtriplem11  12292  pythagtriplem12  12293  pythagtriplem13  12294  pythagtriplem14  12295  pythagtriplem19  12300  pythagtrip  12301  dvdsprmpweqnn  12353  difsqpwdvds  12355  pcfaclem  12365  pcbc  12367  unennn  12416  ptex  12735  imasaddvallemg  12758  fvprif  12785  mgmsscl  12803  insubm  12903  mulginvcom  13053  mulgassr  13066  mulgmodid  13067  quselbasg  13135  ghmnsgima  13168  ringrng  13351  rmodislmodlem  13627  rmodislmod  13628  lssincl  13662  sralmod  13727  rnglidlmmgm  13773  rnglidlmsgrp  13774  rnglidlrng  13775  2idlcpblrng  13799  ntrin  14008  elnei  14036  restco  14058  cnpnei  14103  cncnp2m  14115  sslm  14131  upxp  14156  blres  14318  metcnp3  14395  tgqioo  14431  ptolemy  14629  cxpcom  14741  logbgcd1irr  14769  logbprmirr  14774  lgslem1  14785  lgsneg  14809  lgsdilem  14812  lgsdir  14820  lgssq2  14826  lgsdirnn0  14832