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 )

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced 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  3672  frirrg  4490  breldmg  4982  fntpg  5432  funimaexglem  5459  fex2  5551  fresaunres2disj  5565  fvun1  5763  fprg  5889  fsnunfv  5907  fnfvima  5943  cocan1  5983  cocan2  5984  mpoeq3dv  6144  fovcld  6183  fvmpopr2d  6215  funexw  6331  mpofvex  6431  poxp  6458  suppval1  6469  suppvalfng  6470  suppvalfn  6471  suppimacnvfn  6476  suppsnopdc  6480  smoiso  6563  tfrlem5  6575  tfrlemibxssdm  6588  tfr1onlembfn  6605  tfri1dALT  6612  tfrcllembfn  6618  rdgon  6647  freccllem  6663  nnawordex  6792  1dom1el  7097  mapxpen  7138  fidceq  7161  fidifsnen  7162  dif1en  7173  en2eqpr  7204  unsnfi  7216  unsnfidcex  7217  unsnfidcel  7218  fisseneq  7232  funisfsupp  7281  ordiso2  7365  updjud  7412  mkvprop  7488  endjudisj  7556  xpdjuen  7564  mulcanenq0ec  7802  prltlu  7844  prarloclem3step  7853  prarloclem5  7857  ltasrg  8127  cnegexlem1  8491  addcan  8496  apcotr  8925  apadd1  8926  mulext1  8930  divdivap1  9043  divdivap2  9044  div2negap  9055  divneg2ap  9056  ltmulgt11  9184  ltdiv2  9207  squeeze0  9224  nndivtr  9325  nn0n0n1ge2  9694  zdivmul  9715  gtndiv  9720  eluzuzle  9909  eluzp1p1  9927  qdivcl  10022  irrmul  10026  rpgecl  10062  xaddass  10250  xltadd1  10257  xlt2add  10261  lbico1  10311  lbicc2  10365  zltaddlt1le  10389  uzsubsubfz  10430  elfz1b  10475  elfz0ubfz0  10510  fz0fzelfz0  10512  difelfzle  10519  difelfznle  10520  2ffzeq  10526  fzo1fzo0n0  10573  ubmelfzo  10596  fzonn0p1p1  10609  elfzom1p1elfzo  10610  elfzonelfzo  10626  subfzo0  10639  ceiqle  10728  ceilqle  10729  modqval  10739  flqpmodeq  10742  modq0  10744  negqmod0  10746  modqge0  10747  modqlt  10748  modqdiffl  10750  modqmulnn  10757  modqvalp1  10758  modqmuladdnn0  10783  qnegmod  10784  addmodid  10787  modfzo0difsn  10810  addmodlteq  10813  qexpclz  10975  expgt1  10992  expp1zap  11003  expm1ap  11004  expubnd  11011  bernneq2  11077  expnlbnd  11080  mulsubdivbinom2ap  11127  omgadd  11220  hashun  11223  fihashssdif  11237  hashdifpr  11239  fimaxq  11248  ccatval2  11344  ccatval3  11345  ccatval1lsw  11350  ccatval21sw  11351  ccatass  11354  ccatw2s1leng  11384  ccats1val2  11386  ccat2s1fvwd  11393  fzowrddc  11397  swrdval  11398  swrdclg  11400  swrdval2  11401  swrdnd  11409  swrdlen2  11412  swrdfv2  11413  ccatswrd  11420  pfxn0  11438  pfxsuff1eqwrdeq  11449  swrdswrdlem  11454  ccats1pfxeq  11464  ccats1pfxeqrex  11465  ccatopth2  11467  wrd2ind  11473  pfxccatin12lem3  11482  pfxccat3  11484  swrdccat  11485  pfxccatpfx2  11487  pfxccat3a  11488  swrdccat3b  11490  pfxccatid  11491  ccats1pfxeqbi  11492  shftuz  11560  mulreap  11607  redivap  11617  imdivap  11624  resqrtcl  11773  xrmaxltsup  12002  xrmaxaddlem  12004  xrmaxadd  12005  xrlemininf  12015  xrminltinf  12016  climuni  12037  addcn2  12054  mulcn2  12056  efsub  12426  sin02gt0  12509  cos12dec  12513  dvdsval2  12535  addmodlteqALT  12604  modremain  12674  fldivndvdslt  12682  mulgcdr  12773  gcddiv  12774  rpmulgcd  12781  rplpwr  12782  rppwr  12783  nnminle  12790  qredeq  12852  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  dvdsnprmd  12881  euclemma  12902  prmexpb  12907  qnumdenbi  12948  eulerth  12989  fermltl  12990  prmdiv  12991  hashgcdlem  12994  odzcllem  12999  vfermltl  13008  reumodprminv  13010  modprm0  13011  modprmn0modprm0  13013  coprimeprodsq  13014  pythagtriplem1  13022  pythagtriplem3  13024  pythagtriplem4  13025  pythagtriplem10  13026  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem8  13029  pythagtriplem9  13030  pythagtriplem11  13031  pythagtriplem12  13032  pythagtriplem13  13033  pythagtriplem14  13034  pythagtriplem15  13035  pythagtriplem16  13036  pythagtriplem17  13037  pythagtriplem19  13039  pythagtrip  13040  pcpremul  13050  pcdvdsb  13077  dvdsprmpweqnn  13093  dvdsprmpweqle  13094  difsqpwdvds  13095  pcfaclem  13106  pcbc  13108  4sqlem12  13159  ballotfilemsgt1  13232  ballotfilemieq  13238  ballotfilemfrcn0  13251  unennn  13266  nninfdc  13322  setsex  13362  f1ocpbllem  13608  imasaddfnlemg  13612  imasaddvallemg  13613  ercpbl  13629  erlecpbl  13630  qusaddvallemg  13631  fvprif  13641  xpsfrnel2  13644  plusfvalg  13660  imasmnd  13737  insubm  13769  grpidrcan  13847  grpidlcan  13848  grpsubpropd2  13887  imasgrp2  13890  imasgrp  13891  mulgnnsubcl  13914  mulgnn0subcl  13915  mulgsubcl  13916  mulgaddcom  13926  mulginvcom  13927  mulgnnass  13937  mulgassr  13940  mulgpropdg  13944  submmulg  13946  subgcl  13964  subgsubcl  13965  subgsub  13966  subgmulg  13968  nsgconj  13986  ghmsub  14031  ghmrn  14037  ghmeqker  14051  f1ghm0to0  14052  ablinvadd  14091  ablsub4  14094  abladdsub4  14095  subcmnd  14114  imasabl  14117  gsumconstcmn  14143  pwsinvg  14192  rngcl  14218  imasrng  14230  rng1zrlem  14233  rng1zr  14234  rngen1zr0  14236  srgcl  14248  srg1zr  14265  srgen1zr0  14266  ringcl  14291  crngcom  14292  ringidss  14307  mulgass2  14336  imasring  14342  opprmulg  14349  unitmulclb  14394  unitdvcl  14416  rhmmul  14444  rhmdvdsr  14455  subrngmcl  14490  subrgmcl  14514  subrgdv  14519  subrgugrp  14521  domneq0  14554  scafvalg  14616  lmodprop2d  14657  lssclg  14673  lssvnegcl  14685  lssintclm  14693  sralmod  14759  rnglidlmcl  14789  lidlnegcl  14794  rspssp  14803  rnglidlmsgrp  14806  rnglidlrng  14807  2idlcpblrng  14832  qus2idrng  14834  zndvds  14956  znleval2  14961  psrbaglesupp  14981  psrbaglecl  14983  psrbagaddclfi  14984  psrbagcon  14985  basgen  15104  2basgeng  15106  iuncld  15139  neipsm  15178  opnneissb  15179  opnssneib  15180  iscnp3  15227  cnprcl2k  15230  cnpnei  15243  cncnp2m  15255  cnptoprest  15263  sslm  15271  upxp  15296  cnmpt22  15318  distspace  15359  0met  15408  blvalps  15412  blval  15413  ssblps  15449  ssbl  15450  blpnfctr  15463  blopn  15514  blnei  15516  bdxmet  15525  bdbl  15527  metcnp3  15535  tgqioo  15579  ptolemy  15848  sinq12gt0  15854  sincosq1eq  15863  rpcxpadd  15930  cxpmul  15937  rplogbval  15970  logbleb  15986  logbgcd1irr  15992  logbprmirr  15997  pellexlem1  16005  lgsfvalg  16038  lgsneg1  16058  lgssq  16073  lgsdinn0  16081  gausslemma2dlem1a  16091  2lgs  16137  2lgsoddprmlem2  16139  funvtxdm2domval  16184  funiedgdm2domval  16185  iedgedgg  16216  lpvtx  16234  incistruhgr  16245  ausgrumgrien  16325  ausgrusgrien  16326  umgr2edgneu  16367  ushgredgedg  16381  ushgredgedgloop  16383  usgr2v1e2w  16401  egrsubgr  16418  subumgredg2en  16426  iswlk  16478  wlkl1loop  16513  uspgr2wlkeq  16520  istrl  16540  clwwlkccatlem  16555  clwwlkccat  16556  clwwlknccat  16578  clwwlknonex2lem2  16593  clwwlknonex2  16594  iseupth  16602  eupth2lem3lem6fi  16626  konigsbergssiedgwen  16641  bdfind  16886  repiecele0  16980  repiecege0  16981