Theorem 3ad2ant1 1049

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 276	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant2 1047	1 |- ( ( ph /\ ps /\ th ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp1l  1052  simp1r  1053  simp11  1058  simp12  1059  simp13  1060  simp1ll  1091  simp1lr  1092  simp1rl  1093  simp1rr  1094  simp1l1  1121  simp1l2  1122  simp1l3  1123  simp1r1  1124  simp1r2  1125  simp1r3  1126  simp11l  1139  simp11r  1140  simp12l  1141  simp12r  1142  simp13l  1143  simp13r  1144  simp111  1157  simp112  1158  simp113  1159  simp121  1160  simp122  1161  simp123  1162  simp131  1163  simp132  1164  simp133  1165  3anim123i  1215  3jaao  1349  ceqsalt  2848  sbciegft  3082  reupick2  3519  ifbothdc  3675  ifprdc  3819  frirrg  4495  breldmg  4987  fntpg  5437  funimaexglem  5464  fex2  5556  fresaunres2disj  5570  fvun1  5769  fprg  5898  fsnunfv  5916  fnfvima  5953  cocan1  5993  cocan2  5994  mpoeq3dv  6154  fovcld  6193  fvmpopr2d  6225  funexw  6341  mpofvex  6441  poxp  6468  suppval1  6479  suppvalfng  6480  suppvalfn  6481  suppimacnvfn  6486  suppsnopdc  6490  smoiso  6573  tfrlem5  6585  tfrlemibxssdm  6598  tfr1onlembfn  6615  tfri1dALT  6622  tfrcllembfn  6628  rdgon  6657  freccllem  6673  nnawordex  6802  1dom1el  7107  mapxpen  7148  fidceq  7171  fidifsnen  7172  dif1en  7183  en2eqpr  7214  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  fisseneq  7242  funisfsupp  7291  ordiso2  7375  updjud  7422  mkvprop  7498  endjudisj  7566  xpdjuen  7574  mulcanenq0ec  7812  prltlu  7854  prarloclem3step  7863  prarloclem5  7867  ltasrg  8137  cnegexlem1  8502  addcan  8507  apcotr  8937  apadd1  8938  mulext1  8942  divdivap1  9055  divdivap2  9056  div2negap  9067  divneg2ap  9068  ltmulgt11  9196  ltdiv2  9219  squeeze0  9236  nndivtr  9348  nn0n0n1ge2  9719  zdivmul  9740  gtndiv  9745  eluzuzle  9939  eluzp1p1  9957  qdivcl  10052  irrmul  10057  rpgecl  10093  xaddass  10281  xltadd1  10288  xlt2add  10292  lbico1  10342  lbicc2  10396  zltaddlt1le  10420  uzsubsubfz  10462  elfz1b  10507  elfz0ubfz0  10542  fz0fzelfz0  10544  difelfzle  10551  difelfznle  10552  2ffzeq  10558  fzo1fzo0n0  10605  ubmelfzo  10628  fzonn0p1p1  10641  elfzom1p1elfzo  10642  elfzonelfzo  10658  subfzo0  10671  ceiqle  10763  ceilqle  10764  modqval  10774  flqpmodeq  10777  modq0  10779  negqmod0  10781  modqge0  10782  modqlt  10783  modqdiffl  10785  modqmulnn  10792  modqvalp1  10793  modqmuladdnn0  10818  qnegmod  10819  addmodid  10822  modfzo0difsn  10845  addmodlteq  10848  qexpclz  11010  expgt1  11027  expp1zap  11038  expm1ap  11039  expubnd  11046  bernneq2  11112  expnlbnd  11115  mulsubdivbinom2ap  11163  omgadd  11256  hashun  11259  fihashssdif  11273  hashdifpr  11275  fimaxq  11284  ccatval2  11380  ccatval3  11381  ccatval1lsw  11386  ccatval21sw  11387  ccatass  11390  ccatw2s1leng  11420  ccats1val2  11422  ccat2s1fvwd  11429  fzowrddc  11433  swrdval  11434  swrdclg  11436  swrdval2  11437  swrdnd  11445  swrdlen2  11448  swrdfv2  11449  ccatswrd  11456  pfxn0  11474  pfxsuff1eqwrdeq  11485  swrdswrdlem  11490  ccats1pfxeq  11500  ccats1pfxeqrex  11501  ccatopth2  11503  wrd2ind  11509  pfxccatin12lem3  11518  pfxccat3  11520  swrdccat  11521  pfxccatpfx2  11523  pfxccat3a  11524  swrdccat3b  11526  pfxccatid  11527  ccats1pfxeqbi  11528  shftuz  11596  mulreap  11643  redivap  11653  imdivap  11660  resqrtcl  11809  xrmaxltsup  12040  xrmaxaddlem  12042  xrmaxadd  12043  xrlemininf  12053  xrminltinf  12054  climuni  12075  addcn2  12092  mulcn2  12094  efsub  12464  sin02gt0  12547  cos12dec  12551  dvdsval2  12573  addmodlteqALT  12642  modremain  12712  fldivndvdslt  12720  mulgcdr  12811  gcddiv  12812  rpmulgcd  12819  rplpwr  12820  rppwr  12821  nnminle  12828  qredeq  12890  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  dvdsnprmd  12919  euclemma  12941  prmexpb  12946  qnumdenbi  12988  eulerth  13031  fermltl  13032  prmdiv  13033  hashgcdlem  13036  odzcllem  13041  vfermltl  13050  reumodprminv  13052  modprm0  13053  modprmn0modprm0  13055  coprimeprodsq  13056  pythagtriplem1  13064  pythagtriplem3  13066  pythagtriplem4  13067  pythagtriplem10  13068  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem8  13071  pythagtriplem9  13072  pythagtriplem11  13073  pythagtriplem12  13074  pythagtriplem13  13075  pythagtriplem14  13076  pythagtriplem15  13077  pythagtriplem16  13078  pythagtriplem17  13079  pythagtriplem19  13081  pythagtrip  13082  pcpremul  13092  pcdvdsb  13119  dvdsprmpweqnn  13135  dvdsprmpweqle  13136  difsqpwdvds  13137  pcfaclem  13148  pcbc  13150  4sqlem12  13201  ballotfilemsgt1  13303  ballotfilemieq  13309  ballotfilemfrcn0  13322  unennn  13337  nninfdc  13393  setsex  13433  f1ocpbllem  13680  imasaddfnlemg  13684  imasaddvallemg  13685  ercpbl  13701  erlecpbl  13702  qusaddvallemg  13703  fvprif  13713  xpsfrnel2  13716  plusfvalg  13732  imasmnd  13809  insubm  13841  grpidrcan  13919  grpidlcan  13920  grpsubpropd2  13959  imasgrp2  13962  imasgrp  13963  mulgnnsubcl  13986  mulgnn0subcl  13987  mulgsubcl  13988  mulgaddcom  13998  mulginvcom  13999  mulgnnass  14009  mulgassr  14012  mulgpropdg  14016  submmulg  14018  subgcl  14036  subgsubcl  14037  subgsub  14038  subgmulg  14040  nsgconj  14058  ghmsub  14103  ghmrn  14109  ghmeqker  14123  f1ghm0to0  14124  ablinvadd  14163  ablsub4  14166  abladdsub4  14167  subcmnd  14186  imasabl  14189  gsumconstcmn  14215  pwsinvg  14264  rngcl  14292  imasrng  14304  rng1zrlem  14307  rng1zr  14308  rngen1zr0  14310  srgcl  14323  srg1zr  14340  srgen1zr0  14341  ringcl  14366  crngcom  14367  ringidss  14383  mulgass2  14412  imasring  14418  opprmulg  14425  unitmulclb  14470  unitdvcl  14492  rhmmul  14520  rhmdvdsr  14531  subrngmcl  14566  subrgmcl  14590  subrgdv  14595  subrgugrp  14597  domneq0  14630  scafvalg  14693  lmodprop2d  14734  lssclg  14750  lssvnegcl  14762  lssintclm  14770  sralmod  14836  rnglidlmcl  14866  lidlnegcl  14871  rspssp  14880  rnglidlmsgrp  14883  rnglidlrng  14884  2idlcpblrng  14909  qus2idrng  14911  zndvds  15033  znleval2  15038  assa2ass  15058  assa2ass2  15059  asclmul1  15078  asclmul2  15079  ascldimul  15080  asclmulg  15093  psrbaglesupp  15107  psrbaglecl  15109  psrbagaddclfi  15110  psrbagcon  15111  basgen  15230  2basgeng  15232  iuncld  15265  neipsm  15304  opnneissb  15305  opnssneib  15306  iscnp3  15353  cnprcl2k  15356  cnpnei  15369  cncnp2m  15381  cnptoprest  15389  sslm  15397  upxp  15422  cnmpt22  15444  distspace  15485  0met  15534  blvalps  15538  blval  15539  ssblps  15575  ssbl  15576  blpnfctr  15589  blopn  15640  blnei  15642  bdxmet  15651  bdbl  15653  metcnp3  15661  tgqioo  15705  ptolemy  15975  sinq12gt0  15981  sincosq1eq  15990  rpcxpadd  16060  cxpmul  16067  rplogbval  16100  logbleb  16116  logbgcd1irr  16122  logbprmirr  16127  pellexlem1  16148  ppiqwordi  16174  bcmono  16202  lgsfvalg  16222  lgsneg1  16242  lgssq  16257  lgsdinn0  16265  gausslemma2dlem1a  16275  2lgs  16321  2lgsoddprmlem2  16323  funvtxdm2domval  16368  funiedgdm2domval  16369  iedgedgg  16400  lpvtx  16418  incistruhgr  16429  ausgrumgrien  16509  ausgrusgrien  16510  umgr2edgneu  16551  ushgredgedg  16565  ushgredgedgloop  16567  usgr2v1e2w  16585  egrsubgr  16602  subumgredg2en  16610  iswlk  16662  wlkl1loop  16697  uspgr2wlkeq  16704  istrl  16724  clwwlkccatlem  16739  clwwlkccat  16740  clwwlknccat  16762  clwwlknonex2lem2  16777  clwwlknonex2  16778  iseupth  16786  eupth2lem3lem6fi  16810  konigsbergssiedgwen  16825  bdfind  17070  repiecele0  17173  repiecege0  17174