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  8501  addcan  8506  apcotr  8935  apadd1  8936  mulext1  8940  divdivap1  9053  divdivap2  9054  div2negap  9065  divneg2ap  9066  ltmulgt11  9194  ltdiv2  9217  squeeze0  9234  nndivtr  9346  nn0n0n1ge2  9715  zdivmul  9736  gtndiv  9741  eluzuzle  9930  eluzp1p1  9948  qdivcl  10043  irrmul  10047  rpgecl  10083  xaddass  10271  xltadd1  10278  xlt2add  10282  lbico1  10332  lbicc2  10386  zltaddlt1le  10410  uzsubsubfz  10452  elfz1b  10497  elfz0ubfz0  10532  fz0fzelfz0  10534  difelfzle  10541  difelfznle  10542  2ffzeq  10548  fzo1fzo0n0  10595  ubmelfzo  10618  fzonn0p1p1  10631  elfzom1p1elfzo  10632  elfzonelfzo  10648  subfzo0  10661  ceiqle  10750  ceilqle  10751  modqval  10761  flqpmodeq  10764  modq0  10766  negqmod0  10768  modqge0  10769  modqlt  10770  modqdiffl  10772  modqmulnn  10779  modqvalp1  10780  modqmuladdnn0  10805  qnegmod  10806  addmodid  10809  modfzo0difsn  10832  addmodlteq  10835  qexpclz  10997  expgt1  11014  expp1zap  11025  expm1ap  11026  expubnd  11033  bernneq2  11099  expnlbnd  11102  mulsubdivbinom2ap  11149  omgadd  11242  hashun  11245  fihashssdif  11259  hashdifpr  11261  fimaxq  11270  ccatval2  11366  ccatval3  11367  ccatval1lsw  11372  ccatval21sw  11373  ccatass  11376  ccatw2s1leng  11406  ccats1val2  11408  ccat2s1fvwd  11415  fzowrddc  11419  swrdval  11420  swrdclg  11422  swrdval2  11423  swrdnd  11431  swrdlen2  11434  swrdfv2  11435  ccatswrd  11442  pfxn0  11460  pfxsuff1eqwrdeq  11471  swrdswrdlem  11476  ccats1pfxeq  11486  ccats1pfxeqrex  11487  ccatopth2  11489  wrd2ind  11495  pfxccatin12lem3  11504  pfxccat3  11506  swrdccat  11507  pfxccatpfx2  11509  pfxccat3a  11510  swrdccat3b  11512  pfxccatid  11513  ccats1pfxeqbi  11514  shftuz  11582  mulreap  11629  redivap  11639  imdivap  11646  resqrtcl  11795  xrmaxltsup  12024  xrmaxaddlem  12026  xrmaxadd  12027  xrlemininf  12037  xrminltinf  12038  climuni  12059  addcn2  12076  mulcn2  12078  efsub  12448  sin02gt0  12531  cos12dec  12535  dvdsval2  12557  addmodlteqALT  12626  modremain  12696  fldivndvdslt  12704  mulgcdr  12795  gcddiv  12796  rpmulgcd  12803  rplpwr  12804  rppwr  12805  nnminle  12812  qredeq  12874  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  dvdsnprmd  12903  euclemma  12924  prmexpb  12929  qnumdenbi  12970  eulerth  13011  fermltl  13012  prmdiv  13013  hashgcdlem  13016  odzcllem  13021  vfermltl  13030  reumodprminv  13032  modprm0  13033  modprmn0modprm0  13035  coprimeprodsq  13036  pythagtriplem1  13044  pythagtriplem3  13046  pythagtriplem4  13047  pythagtriplem10  13048  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem8  13051  pythagtriplem9  13052  pythagtriplem11  13053  pythagtriplem12  13054  pythagtriplem13  13055  pythagtriplem14  13056  pythagtriplem15  13057  pythagtriplem16  13058  pythagtriplem17  13059  pythagtriplem19  13061  pythagtrip  13062  pcpremul  13072  pcdvdsb  13099  dvdsprmpweqnn  13115  dvdsprmpweqle  13116  difsqpwdvds  13117  pcfaclem  13128  pcbc  13130  4sqlem12  13181  ballotfilemsgt1  13254  ballotfilemieq  13260  ballotfilemfrcn0  13273  unennn  13288  nninfdc  13344  setsex  13384  f1ocpbllem  13631  imasaddfnlemg  13635  imasaddvallemg  13636  ercpbl  13652  erlecpbl  13653  qusaddvallemg  13654  fvprif  13664  xpsfrnel2  13667  plusfvalg  13683  imasmnd  13760  insubm  13792  grpidrcan  13870  grpidlcan  13871  grpsubpropd2  13910  imasgrp2  13913  imasgrp  13914  mulgnnsubcl  13937  mulgnn0subcl  13938  mulgsubcl  13939  mulgaddcom  13949  mulginvcom  13950  mulgnnass  13960  mulgassr  13963  mulgpropdg  13967  submmulg  13969  subgcl  13987  subgsubcl  13988  subgsub  13989  subgmulg  13991  nsgconj  14009  ghmsub  14054  ghmrn  14060  ghmeqker  14074  f1ghm0to0  14075  ablinvadd  14114  ablsub4  14117  abladdsub4  14118  subcmnd  14137  imasabl  14140  gsumconstcmn  14166  pwsinvg  14215  rngcl  14243  imasrng  14255  rng1zrlem  14258  rng1zr  14259  rngen1zr0  14261  srgcl  14274  srg1zr  14291  srgen1zr0  14292  ringcl  14317  crngcom  14318  ringidss  14334  mulgass2  14363  imasring  14369  opprmulg  14376  unitmulclb  14421  unitdvcl  14443  rhmmul  14471  rhmdvdsr  14482  subrngmcl  14517  subrgmcl  14541  subrgdv  14546  subrgugrp  14548  domneq0  14581  scafvalg  14644  lmodprop2d  14685  lssclg  14701  lssvnegcl  14713  lssintclm  14721  sralmod  14787  rnglidlmcl  14817  lidlnegcl  14822  rspssp  14831  rnglidlmsgrp  14834  rnglidlrng  14835  2idlcpblrng  14860  qus2idrng  14862  zndvds  14984  znleval2  14989  assa2ass  15009  assa2ass2  15010  asclmul1  15029  asclmul2  15030  ascldimul  15031  asclmulg  15044  psrbaglesupp  15058  psrbaglecl  15060  psrbagaddclfi  15061  psrbagcon  15062  basgen  15181  2basgeng  15183  iuncld  15216  neipsm  15255  opnneissb  15256  opnssneib  15257  iscnp3  15304  cnprcl2k  15307  cnpnei  15320  cncnp2m  15332  cnptoprest  15340  sslm  15348  upxp  15373  cnmpt22  15395  distspace  15436  0met  15485  blvalps  15489  blval  15490  ssblps  15526  ssbl  15527  blpnfctr  15540  blopn  15591  blnei  15593  bdxmet  15602  bdbl  15604  metcnp3  15612  tgqioo  15656  ptolemy  15925  sinq12gt0  15931  sincosq1eq  15940  rpcxpadd  16007  cxpmul  16014  rplogbval  16047  logbleb  16063  logbgcd1irr  16069  logbprmirr  16074  pellexlem1  16091  lgsfvalg  16124  lgsneg1  16144  lgssq  16159  lgsdinn0  16167  gausslemma2dlem1a  16177  2lgs  16223  2lgsoddprmlem2  16225  funvtxdm2domval  16270  funiedgdm2domval  16271  iedgedgg  16302  lpvtx  16320  incistruhgr  16331  ausgrumgrien  16411  ausgrusgrien  16412  umgr2edgneu  16453  ushgredgedg  16467  ushgredgedgloop  16469  usgr2v1e2w  16487  egrsubgr  16504  subumgredg2en  16512  iswlk  16564  wlkl1loop  16599  uspgr2wlkeq  16606  istrl  16626  clwwlkccatlem  16641  clwwlkccat  16642  clwwlknccat  16664  clwwlknonex2lem2  16679  clwwlknonex2  16680  iseupth  16688  eupth2lem3lem6fi  16712  konigsbergssiedgwen  16727  bdfind  16972  repiecele0  17075  repiecege0  17076