Theorem 3ad2ant1 1045

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simp1l  1048  simp1r  1049  simp11  1054  simp12  1055  simp13  1056  simp1ll  1087  simp1lr  1088  simp1rl  1089  simp1rr  1090  simp1l1  1117  simp1l2  1118  simp1l3  1119  simp1r1  1120  simp1r2  1121  simp1r3  1122  simp11l  1135  simp11r  1136  simp12l  1137  simp12r  1138  simp13l  1139  simp13r  1140  simp111  1153  simp112  1154  simp113  1155  simp121  1156  simp122  1157  simp123  1158  simp131  1159  simp132  1160  simp133  1161  3anim123i  1211  3jaao  1345  ceqsalt  2830  sbciegft  3063  reupick2  3495  ifbothdc  3644  frirrg  4453  breldmg  4943  fntpg  5393  funimaexglem  5420  fex2  5511  fvun1  5721  fprg  5845  fsnunfv  5863  fnfvima  5899  cocan1  5938  cocan2  5939  mpoeq3dv  6097  fovcld  6136  fvmpopr2d  6168  funexw  6283  mpofvex  6379  poxp  6406  suppval1  6417  suppvalfng  6418  suppvalfn  6419  suppimacnvfn  6424  suppsnopdc  6428  smoiso  6511  tfrlem5  6523  tfrlemibxssdm  6536  tfr1onlembfn  6553  tfri1dALT  6560  tfrcllembfn  6566  rdgon  6595  freccllem  6611  nnawordex  6740  1dom1el  7036  mapxpen  7077  fidceq  7099  fidifsnen  7100  dif1en  7111  en2eqpr  7142  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  fisseneq  7170  funisfsupp  7216  ordiso2  7294  updjud  7341  mkvprop  7417  endjudisj  7485  xpdjuen  7493  mulcanenq0ec  7725  prltlu  7767  prarloclem3step  7776  prarloclem5  7780  ltasrg  8050  cnegexlem1  8413  addcan  8418  apcotr  8846  apadd1  8847  mulext1  8851  divdivap1  8962  divdivap2  8963  div2negap  8974  divneg2ap  8975  ltmulgt11  9103  ltdiv2  9126  squeeze0  9143  nndivtr  9244  nn0n0n1ge2  9611  zdivmul  9631  gtndiv  9636  eluzuzle  9825  eluzp1p1  9843  qdivcl  9938  irrmul  9942  rpgecl  9978  xaddass  10165  xltadd1  10172  xlt2add  10176  lbico1  10226  lbicc2  10280  zltaddlt1le  10304  uzsubsubfz  10344  elfz1b  10387  elfz0ubfz0  10422  fz0fzelfz0  10424  difelfzle  10431  difelfznle  10432  2ffzeq  10438  fzo1fzo0n0  10485  ubmelfzo  10508  fzonn0p1p1  10521  elfzom1p1elfzo  10522  elfzonelfzo  10538  subfzo0  10551  ceiqle  10638  ceilqle  10639  modqval  10649  flqpmodeq  10652  modq0  10654  negqmod0  10656  modqge0  10657  modqlt  10658  modqdiffl  10660  modqmulnn  10667  modqvalp1  10668  modqmuladdnn0  10693  qnegmod  10694  addmodid  10697  modfzo0difsn  10720  addmodlteq  10723  qexpclz  10885  expgt1  10902  expp1zap  10913  expm1ap  10914  expubnd  10921  bernneq2  10986  expnlbnd  10989  mulsubdivbinom2ap  11036  omgadd  11128  hashun  11131  fihashssdif  11145  hashdifpr  11147  fimaxq  11154  ccatval2  11241  ccatval3  11242  ccatval1lsw  11247  ccatval21sw  11248  ccatass  11251  ccatw2s1leng  11281  ccats1val2  11283  ccat2s1fvwd  11290  fzowrddc  11294  swrdval  11295  swrdclg  11297  swrdval2  11298  swrdnd  11306  swrdlen2  11309  swrdfv2  11310  ccatswrd  11317  pfxn0  11335  pfxsuff1eqwrdeq  11346  swrdswrdlem  11351  ccats1pfxeq  11361  ccats1pfxeqrex  11362  ccatopth2  11364  wrd2ind  11370  pfxccatin12lem3  11379  pfxccat3  11381  swrdccat  11382  pfxccatpfx2  11384  pfxccat3a  11385  swrdccat3b  11387  pfxccatid  11388  ccats1pfxeqbi  11389  shftuz  11457  mulreap  11504  redivap  11514  imdivap  11521  resqrtcl  11669  xrmaxltsup  11898  xrmaxaddlem  11900  xrmaxadd  11901  xrlemininf  11911  xrminltinf  11912  climuni  11933  addcn2  11950  mulcn2  11952  efsub  12322  sin02gt0  12405  cos12dec  12409  dvdsval2  12431  addmodlteqALT  12500  modremain  12570  fldivndvdslt  12578  mulgcdr  12669  gcddiv  12670  rpmulgcd  12677  rplpwr  12678  rppwr  12679  nnminle  12686  qredeq  12748  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  dvdsnprmd  12777  euclemma  12798  prmexpb  12803  qnumdenbi  12844  eulerth  12885  fermltl  12886  prmdiv  12887  hashgcdlem  12890  odzcllem  12895  vfermltl  12904  reumodprminv  12906  modprm0  12907  modprmn0modprm0  12909  coprimeprodsq  12910  pythagtriplem1  12918  pythagtriplem3  12920  pythagtriplem4  12921  pythagtriplem10  12922  pythagtriplem6  12923  pythagtriplem7  12924  pythagtriplem8  12925  pythagtriplem9  12926  pythagtriplem11  12927  pythagtriplem12  12928  pythagtriplem13  12929  pythagtriplem14  12930  pythagtriplem15  12931  pythagtriplem16  12932  pythagtriplem17  12933  pythagtriplem19  12935  pythagtrip  12936  pcpremul  12946  pcdvdsb  12973  dvdsprmpweqnn  12989  dvdsprmpweqle  12990  difsqpwdvds  12991  pcfaclem  13002  pcbc  13004  4sqlem12  13055  unennn  13098  nninfdc  13154  setsex  13194  f1ocpbllem  13473  imasaddfnlemg  13477  imasaddvallemg  13478  ercpbl  13494  erlecpbl  13495  qusaddvallemg  13496  fvprif  13506  xpsfrnel2  13509  plusfvalg  13526  imasmnd  13616  insubm  13648  grpidrcan  13728  grpidlcan  13729  grpsubpropd2  13768  pwsinvg  13775  imasgrp2  13777  imasgrp  13778  mulgnnsubcl  13801  mulgnn0subcl  13802  mulgsubcl  13803  mulgaddcom  13813  mulginvcom  13814  mulgnnass  13824  mulgassr  13827  mulgpropdg  13831  submmulg  13833  subgcl  13851  subgsubcl  13852  subgsub  13853  subgmulg  13855  nsgconj  13873  ghmsub  13918  ghmrn  13924  ghmeqker  13938  f1ghm0to0  13939  ablinvadd  13977  ablsub4  13980  abladdsub4  13981  subcmnd  14000  imasabl  14003  rngcl  14038  imasrng  14050  srgcl  14064  srg1zr  14081  srgen1zr  14082  ringcl  14107  crngcom  14108  ringidss  14123  mulgass2  14152  imasring  14158  opprmulg  14165  unitmulclb  14209  unitdvcl  14231  rhmmul  14259  rhmdvdsr  14270  subrngmcl  14304  subrgmcl  14328  subrgdv  14333  subrgugrp  14335  domneq0  14368  scafvalg  14403  lmodprop2d  14444  lssclg  14460  lssvnegcl  14472  lssintclm  14480  sralmod  14546  rnglidlmcl  14576  lidlnegcl  14581  rspssp  14590  rnglidlmsgrp  14593  rnglidlrng  14594  2idlcpblrng  14619  qus2idrng  14621  zndvds  14745  znleval2  14750  psrbaglesupp  14769  psrbaglecl  14771  psrbagcon  14772  basgen  14891  2basgeng  14893  iuncld  14926  neipsm  14965  opnneissb  14966  opnssneib  14967  iscnp3  15014  cnprcl2k  15017  cnpnei  15030  cncnp2m  15042  cnptoprest  15050  sslm  15058  upxp  15083  cnmpt22  15105  distspace  15146  0met  15195  blvalps  15199  blval  15200  ssblps  15236  ssbl  15237  blpnfctr  15250  blopn  15301  blnei  15303  bdxmet  15312  bdbl  15314  metcnp3  15322  tgqioo  15366  ptolemy  15635  sinq12gt0  15641  sincosq1eq  15650  rpcxpadd  15716  cxpmul  15723  rplogbval  15756  logbleb  15772  logbgcd1irr  15778  logbprmirr  15783  pellexlem1  15791  lgsfvalg  15824  lgsneg1  15844  lgssq  15859  lgsdinn0  15867  gausslemma2dlem1a  15877  2lgs  15923  2lgsoddprmlem2  15925  funvtxdm2domval  15970  funiedgdm2domval  15971  iedgedgg  16002  lpvtx  16020  incistruhgr  16031  ausgrumgrien  16111  ausgrusgrien  16112  umgr2edgneu  16153  ushgredgedg  16167  ushgredgedgloop  16169  usgr2v1e2w  16187  egrsubgr  16204  subumgredg2en  16212  iswlk  16264  wlkl1loop  16299  uspgr2wlkeq  16306  istrl  16326  clwwlkccatlem  16341  clwwlkccat  16342  clwwlknccat  16364  clwwlknonex2lem2  16379  clwwlknonex2  16380  iseupth  16388  eupth2lem3lem6fi  16412  konigsbergssiedgwen  16427  bdfind  16662  repiecele0  16758  repiecege0  16759