Theorem 3adant3 1020

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 997	. 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 981

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 983

This theorem is referenced by:  stoic4a  1452  stoic4b  1453  vtoclgft  2823  eqeu  2943  tpssi  3800  issod  4367  sotricim  4371  soinxp  4746  funopg  5306  fnco  5385  resasplitss  5457  resdif  5546  fnimapr  5641  ftpg  5770  fsnunfv  5787  fvpr1g  5792  fvpr2g  5793  f1ocnvfvb  5851  f1oiso2  5898  moriotass  5930  f1ofveu  5934  acexmid  5945  ovig  6069  ov6g  6086  ovg  6087  ot1stg  6240  ot2ndg  6241  poxp  6320  brtposg  6342  smores3  6381  smoiso  6390  rdgivallem  6469  frecsuclem  6494  nnaord  6597  nnaword  6599  nnawordex  6617  ecopovtrn  6721  ecopovtrng  6724  xpdom3m  6931  mapxpen  6947  sbthlemi4  7064  djuenun  7326  netap  7368  2omotaplemap  7371  ltsopi  7435  addcanpig  7449  distrnqg  7502  ltsonq  7513  ltanqg  7515  ltmnqg  7516  nnanq0  7573  distrnq0  7574  distnq0r  7578  prarloclem  7616  genpassl  7639  genpassu  7640  distrlem1prl  7697  distrlem1pru  7698  distrlem5prl  7701  distrlem5pru  7702  1idprl  7705  1idpru  7706  ltpopr  7710  ltsopr  7711  ltexprlemm  7715  ltexprlemfl  7724  ltexprlemfu  7726  addcanprlemu  7730  recexprlem1ssl  7748  recexprlem1ssu  7749  aptipr  7756  lttrsr  7877  ltsosr  7879  ltasrg  7885  recexgt0sr  7888  mulextsr1  7896  axmulass  7988  ltxrlt  8140  axltwlin  8142  axlttrn  8143  axltadd  8144  letr  8157  mul12  8203  add12  8232  subadd  8277  addsub  8285  npncan  8295  nppcan  8296  nnpcan  8297  nppcan3  8298  pnpcan  8313  pnncan  8315  ppncan  8316  subdi  8459  ltaddsub2  8512  leaddsub2  8514  ltaddsublt  8646  apreap  8662  lemul1  8668  reapmul1lem  8669  reapadd1  8671  reapcotr  8673  receuap  8744  divassap  8765  div23ap  8766  divmulassap  8770  divmulasscomap  8771  divcanap4  8774  divsubdirap  8783  divcanap5  8789  divdiv32ap  8795  divdivap2  8799  div2subap  8912  letrp1  8923  ltmulgt12  8940  lediv1  8944  ltdiv2  8962  lediv2  8966  lbinfle  9025  difgtsumgt  9444  xrletr  9932  xrre2  9945  xaddass  9993  ixxdisj  10027  ubioc1  10053  lbico1  10054  elioo5  10057  iccsupr  10090  lbicc2  10108  ubicc2  10109  iccneg  10113  icoshft  10114  icodisj  10116  iccf1o  10128  iccen  10130  zltaddlt1le  10131  fztri3or  10163  fzdcel  10164  fzen  10167  uzsubsubfz  10171  fzrevral2  10230  fzshftral  10232  fz0fzdiffz0  10254  difelfznle  10259  fzo1fzo0n0  10309  fzonmapblen  10313  fzosubel2  10326  ubmelfzo  10331  elfzodifsumelfzo  10332  ssfzo12bi  10356  ubmelm1fzo  10357  subfzo0  10373  ceiqle  10460  modqid2  10498  zmodidfzoimp  10501  addmodidr  10520  modfzo0difsn  10542  addmodlteq  10545  frec2uzf1od  10553  exprecap  10727  expdivap  10737  expubnd  10743  sqdivap  10750  mulbinom2  10803  bernneq2  10808  mulsubdivbinom2ap  10858  bcval3  10898  bccmpl  10901  omgadd  10949  ccatval1  11056  ccatval2  11057  ccatass  11067  lswccatn0lsw  11070  ccatws1lenp1bg  11092  pfxfv  11138  pfxnd  11143  pfxtrcfv  11147  pfxsuffeqwrdeq  11152  shftval2  11170  mulreap  11208  elicc4abs  11438  abssubge0  11446  abssuble0  11447  maxleast  11557  maxltsup  11562  xrmaxltsup  11602  xrmineqinf  11613  xrltmininf  11614  xrlemininf  11615  fsumdifsnconst  11799  prodfap0  11889  prodfrecap  11890  fprodabs  11960  sin01gt0  12106  cos01gt0  12107  sin02gt0  12108  dvdscmul  12162  summodnegmod  12166  modmulconst  12167  dvdsleabs  12189  dvdsleabs2  12190  addmodlteqALT  12203  dvdsexp  12205  mulmoddvds  12207  divalgb  12269  divgcdz  12325  gcdass  12369  mulgcdr  12372  gcddiv  12373  uzwodc  12391  lcmass  12440  coprmdvds  12447  qredeq  12451  qredeu  12452  congr  12455  divgcdcoprm0  12456  divgcdcoprmex  12457  cncongr1  12458  cncongr2  12459  isprm3  12473  dvdsnprmd  12480  euclemma  12501  prmdvdsexpb  12504  prmexpb  12506  rpexp  12508  znege1  12533  modprminv  12605  modprminveq  12606  vfermltl  12607  modprm0  12610  modprmn0modprm0  12612  coprimeprodsq  12613  coprimeprodsq2  12614  pythagtriplem1  12621  pythagtriplem3  12623  pythagtriplem6  12626  pythagtriplem12  12631  pythagtriplem13  12632  pythagtriplem14  12633  pythagtriplem16  12635  pythagtriplem19  12638  pythagtrip  12639  pcmul  12657  pcdiv  12658  pcqcl  12662  pcgcd1  12684  pcgcd  12685  dvdsprmpweq  12691  difsqpwdvds  12694  pcfaclem  12705  unbendc  12858  strle3g  12973  ercpbl  13196  grpinvid1  13417  grpinvid2  13418  grpasscan1  13428  grpasscan2  13429  grpidrcan  13430  grpidlcan  13431  grpinvadd  13443  grpsubadd  13453  grppncan  13456  pwsinvg  13477  qussub  13606  subcmnd  13702  mulgass2  13853  dvrcan1  13935  dvrcan3  13936  rmodislmodlem  14145  rmodislmod  14146  islssm  14152  lsselg  14156  lspss  14194  lspssp  14198  lsslsp  14224  islidlm  14274  lidlnegcl  14280  lidlsubcl  14282  zndvds  14444  basgen  14585  clsss  14623  ntrin  14629  ntrcls0  14636  neiint  14650  neiss  14655  neipsm  14659  opnssneib  14661  innei  14668  restco  14679  iscnp  14704  cnconst2  14738  txcn  14780  psmetsym  14834  psmetlecl  14839  distspace  14840  xmetlecl  14872  xmetsym  14873  xblcntrps  14918  xblcntr  14919  blssec  14943  blpnfctr  14944  txmetcn  15024  cnmet  15035  dvid  15200  dvidre  15202  dvply1  15270  ptolemy  15329  sinq12gt0  15335  sincosq1eq  15344  rpcxpsub  15413  relogbexpap  15463  logbleb  15466  logblt  15467  rplogbcxp  15468  lgsval4  15530  lgsmod  15536  lgsne0  15548  lgsmulsqcoprm  15556  2lgsoddprmlem1  15615  structiedg0val  15670