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  3558  frirrg  4335  breldmg  4817  fntpg  5254  funimaexglem  5281  fex2  5366  fvun1  5562  fprg  5679  fsnunfv  5697  fnfvima  5730  cocan1  5766  cocan2  5767  mpoeq3dv  5919  funexw  6091  mpofvex  6182  poxp  6211  smoiso  6281  tfrlem5  6293  tfrlemibxssdm  6306  tfr1onlembfn  6323  tfri1dALT  6330  tfrcllembfn  6336  rdgon  6365  freccllem  6381  nnawordex  6508  mapxpen  6826  fidceq  6847  fidifsnen  6848  dif1en  6857  en2eqpr  6885  unsnfi  6896  unsnfidcex  6897  unsnfidcel  6898  fisseneq  6909  ordiso2  7012  updjud  7059  mkvprop  7134  endjudisj  7187  xpdjuen  7195  mulcanenq0ec  7407  prltlu  7449  prarloclem3step  7458  prarloclem5  7462  ltasrg  7732  cnegexlem1  8094  addcan  8099  apcotr  8526  apadd1  8527  mulext1  8531  divdivap1  8640  divdivap2  8641  div2negap  8652  divneg2ap  8653  ltmulgt11  8780  ltdiv2  8803  squeeze0  8820  nndivtr  8920  nn0n0n1ge2  9282  zdivmul  9302  gtndiv  9307  eluzuzle  9495  eluzp1p1  9512  qdivcl  9602  irrmul  9606  rpgecl  9639  xaddass  9826  xltadd1  9833  xlt2add  9837  lbico1  9887  lbicc2  9941  zltaddlt1le  9964  uzsubsubfz  10003  elfz1b  10046  elfz0ubfz0  10081  fz0fzelfz0  10083  difelfzle  10090  difelfznle  10091  2ffzeq  10097  fzo1fzo0n0  10139  ubmelfzo  10156  fzonn0p1p1  10169  elfzom1p1elfzo  10170  elfzonelfzo  10186  subfzo0  10198  ceiqle  10269  ceilqle  10270  modqval  10280  flqpmodeq  10283  modq0  10285  negqmod0  10287  modqge0  10288  modqlt  10289  modqdiffl  10291  modqmulnn  10298  modqvalp1  10299  modqmuladdnn0  10324  qnegmod  10325  addmodid  10328  modfzo0difsn  10351  addmodlteq  10354  qexpclz  10497  expgt1  10514  expp1zap  10525  expm1ap  10526  expubnd  10533  bernneq2  10597  expnlbnd  10600  omgadd  10737  hashun  10740  fihashssdif  10753  hashdifpr  10755  fimaxq  10762  shftuz  10781  mulreap  10828  redivap  10838  imdivap  10845  resqrtcl  10993  xrmaxltsup  11221  xrmaxaddlem  11223  xrmaxadd  11224  xrlemininf  11234  xrminltinf  11235  climuni  11256  addcn2  11273  mulcn2  11275  efsub  11644  sin02gt0  11726  cos12dec  11730  dvdsval2  11752  addmodlteqALT  11819  modremain  11888  fldivndvdslt  11894  mulgcdr  11973  gcddiv  11974  rpmulgcd  11981  rplpwr  11982  rppwr  11983  nnminle  11990  qredeq  12050  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  dvdsnprmd  12079  euclemma  12100  prmexpb  12105  qnumdenbi  12146  eulerth  12187  fermltl  12188  prmdiv  12189  hashgcdlem  12192  odzcllem  12196  vfermltl  12205  reumodprminv  12207  modprm0  12208  modprmn0modprm0  12210  coprimeprodsq  12211  pythagtriplem1  12219  pythagtriplem3  12221  pythagtriplem4  12222  pythagtriplem10  12223  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem8  12226  pythagtriplem9  12227  pythagtriplem11  12228  pythagtriplem12  12229  pythagtriplem13  12230  pythagtriplem14  12231  pythagtriplem15  12232  pythagtriplem16  12233  pythagtriplem17  12234  pythagtriplem19  12236  pythagtrip  12237  pcpremul  12247  pcdvdsb  12273  dvdsprmpweqnn  12289  dvdsprmpweqle  12290  difsqpwdvds  12291  pcfaclem  12301  pcbc  12303  unennn  12352  nninfdc  12408  setsex  12448  plusfvalg  12617  insubm  12703  grpidrcan  12764  grpidlcan  12765  basgen  12874  2basgeng  12876  iuncld  12909  neipsm  12948  opnneissb  12949  opnssneib  12950  iscnp3  12997  cnprcl2k  13000  cnpnei  13013  cncnp2m  13025  cnptoprest  13033  sslm  13041  upxp  13066  cnmpt22  13088  distspace  13129  0met  13178  blvalps  13182  blval  13183  ssblps  13219  ssbl  13220  blpnfctr  13233  blopn  13284  blnei  13286  bdxmet  13295  bdbl  13297  metcnp3  13305  tgqioo  13341  ptolemy  13539  sinq12gt0  13545  sincosq1eq  13554  rpcxpadd  13620  cxpmul  13627  rplogbval  13657  logbleb  13673  logbgcd1irr  13679  logbprmirr  13684  lgsfvalg  13700  lgsneg1  13720  lgssq  13735  lgsdinn0  13743  bdfind  13981