Theorem 3adant3 1044

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	|- ( ( ph /\ ps ) -> ch )

Assertion

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

Proof of Theorem 3adant3

Step	Hyp	Ref	Expression
1		3simpa 1021	. 2 |- ( ( ph /\ ps /\ th ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( ph /\ ps /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  stoic4a  1477  stoic4b  1478  vtoclgft  2867  eqeu  2990  ssprsseq  3861  tpssi  3868  issod  4445  sotricim  4449  soinxp  4825  funopg  5391  fnco  5471  resasplitss  5549  resdif  5641  fnimapr  5742  ftpg  5873  fsnunfv  5890  fvpr1g  5895  fvpr2g  5896  f1ocnvfvb  5959  f1oiso2  6006  moriotass  6042  f1ofveu  6046  acexmid  6057  ovig  6183  ov6g  6200  ovg  6201  ot1stg  6359  ot2ndg  6360  poxp  6441  suppvalfn  6454  suppsnopdc  6463  suppfnss  6470  funsssuppss  6471  brtposg  6498  smores3  6537  smoiso  6546  rdgivallem  6625  frecsuclem  6650  nnaord  6755  nnaword  6757  nnawordex  6775  ecopovtrn  6879  ecopovtrng  6882  xpdom3m  7098  mapxpen  7114  sbthlemi4  7243  djuenun  7532  netap  7584  2omotaplemap  7587  ltsopi  7651  addcanpig  7665  distrnqg  7718  ltsonq  7729  ltanqg  7731  ltmnqg  7732  nnanq0  7789  distrnq0  7790  distnq0r  7794  prarloclem  7832  genpassl  7855  genpassu  7856  distrlem1prl  7913  distrlem1pru  7914  distrlem5prl  7917  distrlem5pru  7918  1idprl  7921  1idpru  7922  ltpopr  7926  ltsopr  7927  ltexprlemm  7931  ltexprlemfl  7940  ltexprlemfu  7942  addcanprlemu  7946  recexprlem1ssl  7964  recexprlem1ssu  7965  aptipr  7972  lttrsr  8093  ltsosr  8095  ltasrg  8101  recexgt0sr  8104  mulextsr1  8112  axmulass  8204  ltxrlt  8355  axltwlin  8357  axlttrn  8358  axltadd  8359  letr  8372  mul12  8418  add12  8447  subadd  8492  addsub  8500  npncan  8510  nppcan  8511  nnpcan  8512  nppcan3  8513  pnpcan  8528  pnncan  8530  ppncan  8531  subdi  8675  ltaddsub2  8728  leaddsub2  8730  ltaddsublt  8862  apreap  8878  lemul1  8884  reapmul1lem  8885  reapadd1  8887  reapcotr  8889  receuap  8960  divassap  8981  div23ap  8982  divmulassap  8986  divmulasscomap  8987  divcanap4  8990  divsubdirap  8999  divcanap5  9005  divdiv32ap  9011  divdivap2  9015  div2subap  9128  letrp1  9139  ltmulgt12  9156  lediv1  9160  ltdiv2  9178  lediv2  9182  lbinfle  9241  difgtsumgt  9664  xrletr  10160  xrre2  10173  xaddass  10221  ixxdisj  10255  ubioc1  10281  lbico1  10282  elioo5  10285  iccsupr  10318  lbicc2  10336  ubicc2  10337  iccneg  10341  icoshft  10342  icodisj  10344  lincmble  10356  iccf1o  10357  iccen  10359  zltaddlt1le  10360  fztri3or  10393  fzdcel  10394  fzen  10397  uzsubsubfz  10401  fzrevral2  10462  fzshftral  10464  fz0fzdiffz0  10486  difelfznle  10491  fzo1fzo0n0  10544  fzonmapblen  10548  fzosubel2  10562  ubmelfzo  10567  elfzodifsumelfzo  10568  ssfzo12bi  10592  ubmelm1fzo  10593  subfzo0  10610  ceiqle  10699  modqid2  10737  zmodidfzoimp  10740  addmodidr  10759  modfzo0difsn  10781  addmodlteq  10784  frec2uzf1od  10792  exprecap  10966  expdivap  10976  expubnd  10982  sqdivap  10989  mulbinom2  11042  bernneq2  11048  mulsubdivbinom2ap  11098  bcval3  11138  bccmpl  11141  omgadd  11191  ccatval1  11310  ccatval2  11311  ccatass  11321  lswccatn0lsw  11324  ccatws1lenp1bg  11348  ccatw2s1leng  11351  pfxfv  11401  pfxnd  11406  pfxtrcfv  11410  pfxsuffeqwrdeq  11415  swrdswrd  11422  pfxpfx  11425  ccatopth2  11434  pfxccatin12lem4  11443  pfxccatin12lem1  11445  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  pfxccatpfx1  11453  pfxccatpfx2  11454  s3fv0g  11508  s3fv1g  11509  s3fv2g  11510  shftval2  11536  mulreap  11574  elicc4abs  11804  abssubge0  11812  abssuble0  11813  maxleast  11923  maxltsup  11928  xrmaxltsup  11968  xrmineqinf  11979  xrltmininf  11980  xrlemininf  11981  fsumdifsnconst  12166  prodfap0  12256  prodfrecap  12257  fprodabs  12327  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  dvdscmul  12529  summodnegmod  12533  modmulconst  12534  dvdsleabs  12556  dvdsleabs2  12557  addmodlteqALT  12570  dvdsexp  12572  mulmoddvds  12574  divalgb  12636  divgcdz  12692  gcdass  12736  mulgcdr  12739  gcddiv  12740  uzwodc  12758  lcmass  12807  coprmdvds  12814  qredeq  12818  qredeu  12819  congr  12822  divgcdcoprm0  12823  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  isprm3  12840  dvdsnprmd  12847  euclemma  12868  prmdvdsexpb  12871  prmexpb  12873  rpexp  12875  znege1  12900  modprminv  12972  modprminveq  12973  vfermltl  12974  modprm0  12977  modprmn0modprm0  12979  coprimeprodsq  12980  coprimeprodsq2  12981  pythagtriplem1  12988  pythagtriplem3  12990  pythagtriplem6  12993  pythagtriplem12  12998  pythagtriplem13  12999  pythagtriplem14  13000  pythagtriplem16  13002  pythagtriplem19  13005  pythagtrip  13006  pcmul  13024  pcdiv  13025  pcqcl  13029  pcgcd1  13051  pcgcd  13052  dvdsprmpweq  13058  difsqpwdvds  13061  pcfaclem  13072  ballotfilemsgt1  13198  ballotfilemrv1  13208  ballotfilemrv2  13209  ballotfilemfrcn0  13217  unbendc  13289  strle3g  13405  ercpbl  13595  grpinvid1  13807  grpinvid2  13808  grpasscan1  13818  grpasscan2  13819  grpidrcan  13820  grpidlcan  13821  grpinvadd  13833  grpsubadd  13843  grppncan  13846  qussub  13990  subcmnd  14086  pwsinvg  14157  rng1zrlem  14198  mulgass2  14301  dvrcan1  14385  dvrcan3  14386  rmodislmodlem  14624  rmodislmod  14625  islssm  14631  lsselg  14635  lspss  14673  lspssp  14677  lsslsp  14703  islidlm  14753  lidlnegcl  14759  lidlsubcl  14761  zndvds  14923  basgen  15071  clsss  15109  ntrin  15115  ntrcls0  15122  neiint  15136  neiss  15141  neipsm  15145  opnssneib  15147  innei  15154  restco  15165  iscnp  15190  cnconst2  15224  txcn  15266  psmetsym  15320  psmetlecl  15325  distspace  15326  xmetlecl  15358  xmetsym  15359  xblcntrps  15404  xblcntr  15405  blssec  15429  blpnfctr  15430  txmetcn  15510  cnmet  15521  dvid  15686  dvidre  15688  dvply1  15756  ptolemy  15815  sinq12gt0  15821  sincosq1eq  15830  rpcxpsub  15899  relogbexpap  15949  logbleb  15952  logblt  15953  rplogbcxp  15954  lgsval4  16019  lgsmod  16025  lgsne0  16037  lgsmulsqcoprm  16045  2lgsoddprmlem1  16104  structiedg0val  16161  lpvtx  16200  upgredg2vtx  16269  upgredgpr  16270  ushgredgedg  16347  ushgredgedgloop  16349  usgr2v1e2w  16367  wlkeq  16475  clwwlkccatlem  16521  clwwlkccat  16522  clwwlkext2edg  16543  clwwlknccat  16544  s2elclwwlknon2  16557  clwwlknonex2lem2  16559  repiecele0  16936  repiecege0  16937