Theorem 3ad2ant3 1047

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	|- ( ph -> ch )

Assertion

Ref	Expression
3ad2ant3	|- ( ( ps /\ th /\ ph ) -> ch )

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantl 277	. 2 |- ( ( th /\ ph ) -> ch )
3	2	3adant1 1042	1 |- ( ( ps /\ th /\ ph ) -> 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:  simp3l  1052  simp3r  1053  simp31  1060  simp32  1061  simp33  1062  simp3ll  1095  simp3lr  1096  simp3rl  1097  simp3rr  1098  simp3l1  1129  simp3l2  1130  simp3l3  1131  simp3r1  1132  simp3r2  1133  simp3r3  1134  simp31l  1147  simp31r  1148  simp32l  1149  simp32r  1150  simp33l  1151  simp33r  1152  simp311  1171  simp312  1172  simp313  1173  simp321  1174  simp322  1175  simp323  1176  simp331  1177  simp332  1178  simp333  1179  3anim123i  1211  3jaao  1345  ceqsalt  2830  ceqsralt  2831  vtoclgft  2855  ifbothdc  3644  ifnebibdc  3655  ssprsseq  3840  tpssi  3847  sotricim  4426  elirr  4645  en2lp  4658  reg3exmidlemwe  4683  sotri2  5141  poltletr  5144  funprg  5387  funtpg  5388  fntpg  5393  funimaexglem  5420  fvun1  5721  ftpg  5846  fsnunf  5862  fsnunfv  5863  caovimo  6226  funsssuppss  6436  brtposg  6463  smoel  6509  rdgivallem  6590  frecsuclem  6615  domssr  6994  mapxpen  7077  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  sbthlemi4  7202  elfir  7232  updjud  7341  ltsopi  7600  distrnqg  7667  ltmnqg  7681  mulcanenq0ec  7725  distrnq0  7739  prarloclem5  7780  1idprl  7870  1idpru  7871  ltaprg  7899  recexprlemopl  7905  recexprlemopu  7907  recexprlem1ssl  7913  aptipr  7921  ltmprr  7922  cauappcvgprlemlol  7927  cauappcvgprlemupu  7929  caucvgprlemlol  7950  caucvgprlemupu  7952  caucvgprprlemlol  7978  caucvgprprlemupu  7980  readdcan  8378  cnegexlem2  8414  addcan2  8419  ltadd2  8658  apreap  8826  ltmul1  8831  apcotr  8846  apadd1  8847  mulext1  8851  divdirap  8936  divcanap5  8953  ltdiv1  9107  lt2halves  9439  zdivmul  9631  eluzsub  9847  ledivge1le  10022  addlelt  10064  xaddass  10165  xleadd1  10171  xltadd1  10172  elioo5  10229  iccsupr  10262  iccneg  10285  icoshft  10286  icoshftf1o  10287  zltaddlt1le  10304  fzen  10340  elfz1b  10387  fzrevral  10402  fzshftral  10405  elfz0ubfz0  10422  elfz0fzfz0  10423  fz0fzelfz0  10424  fz0fzdiffz0  10427  elfzo  10446  fzodcel  10450  elfzonlteqm1  10518  modqaddmulmod  10716  expdivap  10915  leexp2a  10917  bcval3  11076  omgadd  11128  ccatval1  11240  ccatval2  11241  ccatval3  11242  ccatass  11251  ccats1val2  11283  swrdval2  11298  swrdlen  11299  pfxfv  11331  pfxnd  11336  pfxsuffeqwrdeq  11345  swrdswrdlem  11351  swrdswrd  11352  pfxswrd  11353  pfxpfx  11355  ccats1pfxeq  11361  ccats1pfxeqrex  11362  pfxccatin12lem2  11378  pfxccatpfx1  11383  swrdccat3b  11387  pfxccatid  11388  shftfibg  11460  elicc4abs  11734  xrmaxltsup  11898  xrmaxadd  11901  xrlemininf  11911  xrminltinf  11912  mulcn2  11952  fsumsplitsnun  12060  prodfrecap  12187  demoivreALT  12415  dvdsval2  12431  dvdsmodexp  12436  dvdsmulcr  12462  modmulconst  12464  dvdsexp  12502  oddge22np1  12522  modremain  12570  mulgcd  12667  mulgcdr  12669  gcddiv  12670  rpmulgcd  12677  rplpwr  12678  coprmdvds  12744  cncongr1  12755  dvdsnprmd  12777  prmexpb  12803  rpexp  12805  cncongrprm  12809  modprm0  12907  modprmn0modprm0  12909  coprimeprodsq  12910  pythagtriplem1  12918  pythagtriplem3  12920  pythagtriplem10  12922  pythagtriplem6  12923  pythagtriplem11  12927  pythagtriplem12  12928  pythagtriplem13  12929  pythagtriplem15  12931  pythagtriplem17  12933  pythagtriplem19  12935  pcdvdsb  12973  dvdsprmpweqle  12990  pcfaclem  13002  isstructr  13177  setsvala  13193  setsresg  13200  strle3g  13271  imasaddvallemg  13478  fvprif  13506  mgmsscl  13524  insubm  13648  dfgrp3mlem  13761  mulgdirlem  13820  mulgp1  13822  mulgmodid  13828  eqglact  13892  rngdi  14034  rngdir  14035  rmodislmodlem  14446  rmodislmod  14447  lssclg  14460  2idlcpblrng  14619  qusmulrng  14628  clsss  14929  ntrcls0  14942  neiss  14961  neipsm  14965  cnpnei  15030  cncnp2m  15042  cnconst2  15044  sslm  15058  upxp  15083  txmetcn  15330  ptolemy  15635  sincosq1eq  15650  rplogbval  15756  rpcxplogb  15775  pellexlem1  15791  lgsdirprm  15853  lgsdirnn0  15866  gausslemma2dlem1a  15877  gausslemma2dlem3  15882  2lgslem1a1  15905  2lgsoddprmlem1  15924  2lgsoddprmlem2  15925  structiedg0val  15981  lpvtx  16020  incistruhgr  16031  upgredg2vtx  16089  upgredgpr  16090  ausgrumgrien  16111  ausgrusgrien  16112  ushgredgedg  16167  ushgredgedgloop  16169  uhgrissubgr  16202  egrsubgr  16204  0uhgrsubgr  16206  wlkvtxeledgg  16285  wlkeq  16295  wlkl1loop  16299  uspgr2wlkeq  16306  uspgr2wlkeq2  16307  wlkres  16320  loopclwwlkn1b  16360  clwwlkext2edg  16363  clwwlknonex2lem2  16379  clwwlknonex2  16380  clwwlknun  16382  eupth2lem3lem6fi  16412  findset  16661