Theorem 3ad2ant1 1013

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

Syntax hints:   -> wi 4   /\ w3a 973

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 975

This theorem is referenced by:  simp1l  1016  simp1r  1017  simp11  1022  simp12  1023  simp13  1024  simp1ll  1055  simp1lr  1056  simp1rl  1057  simp1rr  1058  simp1l1  1085  simp1l2  1086  simp1l3  1087  simp1r1  1088  simp1r2  1089  simp1r3  1090  simp11l  1103  simp11r  1104  simp12l  1105  simp12r  1106  simp13l  1107  simp13r  1108  simp111  1121  simp112  1122  simp113  1123  simp121  1124  simp122  1125  simp123  1126  simp131  1127  simp132  1128  simp133  1129  3anim123i  1179  3jaao  1303  ceqsalt  2756  sbciegft  2985  reupick2  3413  ifbothdc  3557  frirrg  4333  breldmg  4815  fntpg  5252  funimaexglem  5279  fex2  5364  fvun1  5560  fprg  5676  fsnunfv  5694  fnfvima  5727  cocan1  5763  cocan2  5764  mpoeq3dv  5916  funexw  6088  mpofvex  6179  poxp  6208  smoiso  6278  tfrlem5  6290  tfrlemibxssdm  6303  tfr1onlembfn  6320  tfri1dALT  6327  tfrcllembfn  6333  rdgon  6362  freccllem  6378  nnawordex  6504  mapxpen  6822  fidceq  6843  fidifsnen  6844  dif1en  6853  en2eqpr  6881  unsnfi  6892  unsnfidcex  6893  unsnfidcel  6894  fisseneq  6905  ordiso2  7008  updjud  7055  mkvprop  7130  endjudisj  7174  xpdjuen  7182  mulcanenq0ec  7394  prltlu  7436  prarloclem3step  7445  prarloclem5  7449  ltasrg  7719  cnegexlem1  8081  addcan  8086  apcotr  8513  apadd1  8514  mulext1  8518  divdivap1  8627  divdivap2  8628  div2negap  8639  divneg2ap  8640  ltmulgt11  8767  ltdiv2  8790  squeeze0  8807  nndivtr  8907  nn0n0n1ge2  9269  zdivmul  9289  gtndiv  9294  eluzuzle  9482  eluzp1p1  9499  qdivcl  9589  irrmul  9593  rpgecl  9626  xaddass  9813  xltadd1  9820  xlt2add  9824  lbico1  9874  lbicc2  9928  zltaddlt1le  9951  uzsubsubfz  9990  elfz1b  10033  elfz0ubfz0  10068  fz0fzelfz0  10070  difelfzle  10077  difelfznle  10078  2ffzeq  10084  fzo1fzo0n0  10126  ubmelfzo  10143  fzonn0p1p1  10156  elfzom1p1elfzo  10157  elfzonelfzo  10173  subfzo0  10185  ceiqle  10256  ceilqle  10257  modqval  10267  flqpmodeq  10270  modq0  10272  negqmod0  10274  modqge0  10275  modqlt  10276  modqdiffl  10278  modqmulnn  10285  modqvalp1  10286  modqmuladdnn0  10311  qnegmod  10312  addmodid  10315  modfzo0difsn  10338  addmodlteq  10341  qexpclz  10484  expgt1  10501  expp1zap  10512  expm1ap  10513  expubnd  10520  bernneq2  10584  expnlbnd  10587  omgadd  10724  hashun  10727  fihashssdif  10740  hashdifpr  10742  fimaxq  10749  shftuz  10768  mulreap  10815  redivap  10825  imdivap  10832  resqrtcl  10980  xrmaxltsup  11208  xrmaxaddlem  11210  xrmaxadd  11211  xrlemininf  11221  xrminltinf  11222  climuni  11243  addcn2  11260  mulcn2  11262  efsub  11631  sin02gt0  11713  cos12dec  11717  dvdsval2  11739  addmodlteqALT  11806  modremain  11875  fldivndvdslt  11881  mulgcdr  11960  gcddiv  11961  rpmulgcd  11968  rplpwr  11969  rppwr  11970  nnminle  11977  qredeq  12037  divgcdcoprmex  12043  cncongr1  12044  cncongr2  12045  dvdsnprmd  12066  euclemma  12087  prmexpb  12092  qnumdenbi  12133  eulerth  12174  fermltl  12175  prmdiv  12176  hashgcdlem  12179  odzcllem  12183  vfermltl  12192  reumodprminv  12194  modprm0  12195  modprmn0modprm0  12197  coprimeprodsq  12198  pythagtriplem1  12206  pythagtriplem3  12208  pythagtriplem4  12209  pythagtriplem10  12210  pythagtriplem6  12211  pythagtriplem7  12212  pythagtriplem8  12213  pythagtriplem9  12214  pythagtriplem11  12215  pythagtriplem12  12216  pythagtriplem13  12217  pythagtriplem14  12218  pythagtriplem15  12219  pythagtriplem16  12220  pythagtriplem17  12221  pythagtriplem19  12223  pythagtrip  12224  pcpremul  12234  pcdvdsb  12260  dvdsprmpweqnn  12276  dvdsprmpweqle  12277  difsqpwdvds  12278  pcfaclem  12288  pcbc  12290  unennn  12339  nninfdc  12395  setsex  12435  plusfvalg  12603  insubm  12689  basgen  12795  2basgeng  12797  iuncld  12830  neipsm  12869  opnneissb  12870  opnssneib  12871  iscnp3  12918  cnprcl2k  12921  cnpnei  12934  cncnp2m  12946  cnptoprest  12954  sslm  12962  upxp  12987  cnmpt22  13009  distspace  13050  0met  13099  blvalps  13103  blval  13104  ssblps  13140  ssbl  13141  blpnfctr  13154  blopn  13205  blnei  13207  bdxmet  13216  bdbl  13218  metcnp3  13226  tgqioo  13262  ptolemy  13460  sinq12gt0  13466  sincosq1eq  13475  rpcxpadd  13541  cxpmul  13548  rplogbval  13578  logbleb  13594  logbgcd1irr  13600  logbprmirr  13605  lgsfvalg  13621  lgsneg1  13641  lgssq  13656  lgsdinn0  13664  bdfind  13903