Theorem 3ad2ant1 1002

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2ant1

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantr 274	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant2 1000	1 |- ( ( ph /\ ps /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simp1l  1005  simp1r  1006  simp11  1011  simp12  1012  simp13  1013  simp1ll  1044  simp1lr  1045  simp1rl  1046  simp1rr  1047  simp1l1  1074  simp1l2  1075  simp1l3  1076  simp1r1  1077  simp1r2  1078  simp1r3  1079  simp11l  1092  simp11r  1093  simp12l  1094  simp12r  1095  simp13l  1096  simp13r  1097  simp111  1110  simp112  1111  simp113  1112  simp121  1113  simp122  1114  simp123  1115  simp131  1116  simp132  1117  simp133  1118  3anim123i  1166  3jaao  1286  ceqsalt  2707  sbciegft  2934  reupick2  3357  ifbothdc  3499  frirrg  4267  breldmg  4740  fntpg  5174  funimaexglem  5201  fex2  5286  fvun1  5480  fprg  5596  fsnunfv  5614  fnfvima  5645  cocan1  5681  cocan2  5682  mpoeq3dv  5830  mpofvex  6094  poxp  6122  smoiso  6192  tfrlem5  6204  tfrlemibxssdm  6217  tfr1onlembfn  6234  tfri1dALT  6241  tfrcllembfn  6247  rdgon  6276  freccllem  6292  nnawordex  6417  mapxpen  6735  fidceq  6756  fidifsnen  6757  dif1en  6766  en2eqpr  6794  unsnfi  6800  unsnfidcex  6801  unsnfidcel  6802  fisseneq  6813  ordiso2  6913  updjud  6960  mkvprop  7025  endjudisj  7059  xpdjuen  7067  mulcanenq0ec  7246  prltlu  7288  prarloclem3step  7297  prarloclem5  7301  ltasrg  7571  cnegexlem1  7930  addcan  7935  apcotr  8362  apadd1  8363  mulext1  8367  divdivap1  8476  divdivap2  8477  div2negap  8488  divneg2ap  8489  ltmulgt11  8615  ltdiv2  8638  squeeze0  8655  nndivtr  8755  nn0n0n1ge2  9114  zdivmul  9134  gtndiv  9139  eluzuzle  9327  eluzp1p1  9344  qdivcl  9428  irrmul  9432  rpgecl  9463  xaddass  9645  xltadd1  9652  xlt2add  9656  lbico1  9706  lbicc2  9760  zltaddlt1le  9782  uzsubsubfz  9820  elfz1b  9863  elfz0ubfz0  9895  fz0fzelfz0  9897  difelfzle  9904  difelfznle  9905  2ffzeq  9911  fzo1fzo0n0  9953  ubmelfzo  9970  fzonn0p1p1  9983  elfzom1p1elfzo  9984  elfzonelfzo  10000  subfzo0  10012  ceiqle  10079  ceilqle  10080  modqval  10090  flqpmodeq  10093  modq0  10095  negqmod0  10097  modqge0  10098  modqlt  10099  modqdiffl  10101  modqmulnn  10108  modqvalp1  10109  modqmuladdnn0  10134  qnegmod  10135  addmodid  10138  modfzo0difsn  10161  addmodlteq  10164  qexpclz  10307  expgt1  10324  expp1zap  10335  expm1ap  10336  expubnd  10343  bernneq2  10406  expnlbnd  10409  omgadd  10541  hashun  10544  fihashssdif  10557  hashdifpr  10559  fimaxq  10566  shftuz  10582  mulreap  10629  redivap  10639  imdivap  10646  resqrtcl  10794  xrmaxltsup  11020  xrmaxaddlem  11022  xrmaxadd  11023  xrlemininf  11033  xrminltinf  11034  climuni  11055  addcn2  11072  mulcn2  11074  efsub  11376  sin02gt0  11459  cos12dec  11463  dvdsval2  11485  addmodlteqALT  11546  modremain  11615  fldivndvdslt  11621  mulgcdr  11695  gcddiv  11696  rpmulgcd  11703  rplpwr  11704  rppwr  11705  qredeq  11766  divgcdcoprmex  11772  cncongr1  11773  cncongr2  11774  dvdsnprmd  11795  euclemma  11813  prmexpb  11818  qnumdenbi  11859  hashgcdlem  11892  unennn  11899  setsex  11980  basgen  12238  2basgeng  12240  iuncld  12273  neipsm  12312  opnneissb  12313  opnssneib  12314  iscnp3  12361  cnprcl2k  12364  cnpnei  12377  cncnp2m  12389  cnptoprest  12397  sslm  12405  upxp  12430  cnmpt22  12452  distspace  12493  0met  12542  blvalps  12546  blval  12547  ssblps  12583  ssbl  12584  blpnfctr  12597  blopn  12648  blnei  12650  bdxmet  12659  bdbl  12661  metcnp3  12669  tgqioo  12705  ptolemy  12894  sinq12gt0  12900  sincosq1eq  12909  bdfind  13133