Theorem 3ad2ant1 1044

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  simp1l  1047  simp1r  1048  simp11  1053  simp12  1054  simp13  1055  simp1ll  1086  simp1lr  1087  simp1rl  1088  simp1rr  1089  simp1l1  1116  simp1l2  1117  simp1l3  1118  simp1r1  1119  simp1r2  1120  simp1r3  1121  simp11l  1134  simp11r  1135  simp12l  1136  simp12r  1137  simp13l  1138  simp13r  1139  simp111  1152  simp112  1153  simp113  1154  simp121  1155  simp122  1156  simp123  1157  simp131  1158  simp132  1159  simp133  1160  3anim123i  1210  3jaao  1344  ceqsalt  2829  sbciegft  3062  reupick2  3493  ifbothdc  3640  frirrg  4447  breldmg  4937  fntpg  5386  funimaexglem  5413  fex2  5503  fvun1  5712  fprg  5837  fsnunfv  5855  fnfvima  5889  cocan1  5928  cocan2  5929  mpoeq3dv  6087  fovcld  6126  fvmpopr2d  6158  funexw  6274  mpofvex  6370  poxp  6397  smoiso  6468  tfrlem5  6480  tfrlemibxssdm  6493  tfr1onlembfn  6510  tfri1dALT  6517  tfrcllembfn  6523  rdgon  6552  freccllem  6568  nnawordex  6697  1dom1el  6993  mapxpen  7034  fidceq  7056  fidifsnen  7057  dif1en  7068  en2eqpr  7099  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  fisseneq  7127  ordiso2  7234  updjud  7281  mkvprop  7357  endjudisj  7425  xpdjuen  7433  mulcanenq0ec  7665  prltlu  7707  prarloclem3step  7716  prarloclem5  7720  ltasrg  7990  cnegexlem1  8354  addcan  8359  apcotr  8787  apadd1  8788  mulext1  8792  divdivap1  8903  divdivap2  8904  div2negap  8915  divneg2ap  8916  ltmulgt11  9044  ltdiv2  9067  squeeze0  9084  nndivtr  9185  nn0n0n1ge2  9550  zdivmul  9570  gtndiv  9575  eluzuzle  9764  eluzp1p1  9782  qdivcl  9877  irrmul  9881  rpgecl  9917  xaddass  10104  xltadd1  10111  xlt2add  10115  lbico1  10165  lbicc2  10219  zltaddlt1le  10242  uzsubsubfz  10282  elfz1b  10325  elfz0ubfz0  10360  fz0fzelfz0  10362  difelfzle  10369  difelfznle  10370  2ffzeq  10376  fzo1fzo0n0  10423  ubmelfzo  10446  fzonn0p1p1  10459  elfzom1p1elfzo  10460  elfzonelfzo  10476  subfzo0  10489  ceiqle  10576  ceilqle  10577  modqval  10587  flqpmodeq  10590  modq0  10592  negqmod0  10594  modqge0  10595  modqlt  10596  modqdiffl  10598  modqmulnn  10605  modqvalp1  10606  modqmuladdnn0  10631  qnegmod  10632  addmodid  10635  modfzo0difsn  10658  addmodlteq  10661  qexpclz  10823  expgt1  10840  expp1zap  10851  expm1ap  10852  expubnd  10859  bernneq2  10924  expnlbnd  10927  mulsubdivbinom2ap  10974  omgadd  11066  hashun  11069  fihashssdif  11083  hashdifpr  11085  fimaxq  11092  ccatval2  11179  ccatval3  11180  ccatval1lsw  11185  ccatval21sw  11186  ccatass  11189  ccatw2s1leng  11219  ccats1val2  11221  ccat2s1fvwd  11228  fzowrddc  11232  swrdval  11233  swrdclg  11235  swrdval2  11236  swrdnd  11244  swrdlen2  11247  swrdfv2  11248  ccatswrd  11255  pfxn0  11273  pfxsuff1eqwrdeq  11284  swrdswrdlem  11289  ccats1pfxeq  11299  ccats1pfxeqrex  11300  ccatopth2  11302  wrd2ind  11308  pfxccatin12lem3  11317  pfxccat3  11319  swrdccat  11320  pfxccatpfx2  11322  pfxccat3a  11323  swrdccat3b  11325  pfxccatid  11326  ccats1pfxeqbi  11327  shftuz  11395  mulreap  11442  redivap  11452  imdivap  11459  resqrtcl  11607  xrmaxltsup  11836  xrmaxaddlem  11838  xrmaxadd  11839  xrlemininf  11849  xrminltinf  11850  climuni  11871  addcn2  11888  mulcn2  11890  efsub  12260  sin02gt0  12343  cos12dec  12347  dvdsval2  12369  addmodlteqALT  12438  modremain  12508  fldivndvdslt  12516  mulgcdr  12607  gcddiv  12608  rpmulgcd  12615  rplpwr  12616  rppwr  12617  nnminle  12624  qredeq  12686  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  dvdsnprmd  12715  euclemma  12736  prmexpb  12741  qnumdenbi  12782  eulerth  12823  fermltl  12824  prmdiv  12825  hashgcdlem  12828  odzcllem  12833  vfermltl  12842  reumodprminv  12844  modprm0  12845  modprmn0modprm0  12847  coprimeprodsq  12848  pythagtriplem1  12856  pythagtriplem3  12858  pythagtriplem4  12859  pythagtriplem10  12860  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem8  12863  pythagtriplem9  12864  pythagtriplem11  12865  pythagtriplem12  12866  pythagtriplem13  12867  pythagtriplem14  12868  pythagtriplem15  12869  pythagtriplem16  12870  pythagtriplem17  12871  pythagtriplem19  12873  pythagtrip  12874  pcpremul  12884  pcdvdsb  12911  dvdsprmpweqnn  12927  dvdsprmpweqle  12928  difsqpwdvds  12929  pcfaclem  12940  pcbc  12942  4sqlem12  12993  unennn  13036  nninfdc  13092  setsex  13132  f1ocpbllem  13411  imasaddfnlemg  13415  imasaddvallemg  13416  ercpbl  13432  erlecpbl  13433  qusaddvallemg  13434  fvprif  13444  xpsfrnel2  13447  plusfvalg  13464  imasmnd  13554  insubm  13586  grpidrcan  13666  grpidlcan  13667  grpsubpropd2  13706  pwsinvg  13713  imasgrp2  13715  imasgrp  13716  mulgnnsubcl  13739  mulgnn0subcl  13740  mulgsubcl  13741  mulgaddcom  13751  mulginvcom  13752  mulgnnass  13762  mulgassr  13765  mulgpropdg  13769  submmulg  13771  subgcl  13789  subgsubcl  13790  subgsub  13791  subgmulg  13793  nsgconj  13811  ghmsub  13856  ghmrn  13862  ghmeqker  13876  f1ghm0to0  13877  ablinvadd  13915  ablsub4  13918  abladdsub4  13919  subcmnd  13938  imasabl  13941  rngcl  13976  imasrng  13988  srgcl  14002  srg1zr  14019  srgen1zr  14020  ringcl  14045  crngcom  14046  ringidss  14061  mulgass2  14090  imasring  14096  opprmulg  14103  unitmulclb  14147  unitdvcl  14169  rhmmul  14197  rhmdvdsr  14208  subrngmcl  14242  subrgmcl  14266  subrgdv  14271  subrgugrp  14273  domneq0  14305  scafvalg  14340  lmodprop2d  14381  lssclg  14397  lssvnegcl  14409  lssintclm  14417  sralmod  14483  rnglidlmcl  14513  lidlnegcl  14518  rspssp  14527  rnglidlmsgrp  14530  rnglidlrng  14531  2idlcpblrng  14556  qus2idrng  14558  zndvds  14682  znleval2  14687  basgen  14823  2basgeng  14825  iuncld  14858  neipsm  14897  opnneissb  14898  opnssneib  14899  iscnp3  14946  cnprcl2k  14949  cnpnei  14962  cncnp2m  14974  cnptoprest  14982  sslm  14990  upxp  15015  cnmpt22  15037  distspace  15078  0met  15127  blvalps  15131  blval  15132  ssblps  15168  ssbl  15169  blpnfctr  15182  blopn  15233  blnei  15235  bdxmet  15244  bdbl  15246  metcnp3  15254  tgqioo  15298  ptolemy  15567  sinq12gt0  15573  sincosq1eq  15582  rpcxpadd  15648  cxpmul  15655  rplogbval  15688  logbleb  15704  logbgcd1irr  15710  logbprmirr  15715  lgsfvalg  15753  lgsneg1  15773  lgssq  15788  lgsdinn0  15796  gausslemma2dlem1a  15806  2lgs  15852  2lgsoddprmlem2  15854  funvtxdm2domval  15899  funiedgdm2domval  15900  iedgedgg  15931  lpvtx  15949  incistruhgr  15960  ausgrumgrien  16040  ausgrusgrien  16041  umgr2edgneu  16082  ushgredgedg  16096  ushgredgedgloop  16098  usgr2v1e2w  16116  egrsubgr  16133  subumgredg2en  16141  iswlk  16193  wlkl1loop  16228  uspgr2wlkeq  16235  istrl  16255  clwwlkccatlem  16270  clwwlkccat  16271  clwwlknccat  16293  clwwlknonex2lem2  16308  clwwlknonex2  16309  iseupth  16317  eupth2lem3lem6fi  16341  konigsbergssiedgwen  16356  bdfind  16592