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  2855  eqeu  2977  ssprsseq  3840  tpssi  3847  issod  4422  sotricim  4426  soinxp  4802  funopg  5367  fnco  5447  resasplitss  5524  resdif  5614  fnimapr  5715  ftpg  5846  fsnunfv  5863  fvpr1g  5868  fvpr2g  5869  f1ocnvfvb  5931  f1oiso2  5978  moriotass  6012  f1ofveu  6016  acexmid  6027  ovig  6153  ov6g  6170  ovg  6171  ot1stg  6324  ot2ndg  6325  poxp  6406  suppvalfn  6419  suppsnopdc  6428  suppfnss  6435  funsssuppss  6436  brtposg  6463  smores3  6502  smoiso  6511  rdgivallem  6590  frecsuclem  6615  nnaord  6720  nnaword  6722  nnawordex  6740  ecopovtrn  6844  ecopovtrng  6847  xpdom3m  7061  mapxpen  7077  sbthlemi4  7202  djuenun  7487  netap  7533  2omotaplemap  7536  ltsopi  7600  addcanpig  7614  distrnqg  7667  ltsonq  7678  ltanqg  7680  ltmnqg  7681  nnanq0  7738  distrnq0  7739  distnq0r  7743  prarloclem  7781  genpassl  7804  genpassu  7805  distrlem1prl  7862  distrlem1pru  7863  distrlem5prl  7866  distrlem5pru  7867  1idprl  7870  1idpru  7871  ltpopr  7875  ltsopr  7876  ltexprlemm  7880  ltexprlemfl  7889  ltexprlemfu  7891  addcanprlemu  7895  recexprlem1ssl  7913  recexprlem1ssu  7914  aptipr  7921  lttrsr  8042  ltsosr  8044  ltasrg  8050  recexgt0sr  8053  mulextsr1  8061  axmulass  8153  ltxrlt  8304  axltwlin  8306  axlttrn  8307  axltadd  8308  letr  8321  mul12  8367  add12  8396  subadd  8441  addsub  8449  npncan  8459  nppcan  8460  nnpcan  8461  nppcan3  8462  pnpcan  8477  pnncan  8479  ppncan  8480  subdi  8623  ltaddsub2  8676  leaddsub2  8678  ltaddsublt  8810  apreap  8826  lemul1  8832  reapmul1lem  8833  reapadd1  8835  reapcotr  8837  receuap  8908  divassap  8929  div23ap  8930  divmulassap  8934  divmulasscomap  8935  divcanap4  8938  divsubdirap  8947  divcanap5  8953  divdiv32ap  8959  divdivap2  8963  div2subap  9076  letrp1  9087  ltmulgt12  9104  lediv1  9108  ltdiv2  9126  lediv2  9130  lbinfle  9189  difgtsumgt  9610  xrletr  10104  xrre2  10117  xaddass  10165  ixxdisj  10199  ubioc1  10225  lbico1  10226  elioo5  10229  iccsupr  10262  lbicc2  10280  ubicc2  10281  iccneg  10285  icoshft  10286  icodisj  10288  lincmble  10300  iccf1o  10301  iccen  10303  zltaddlt1le  10304  fztri3or  10336  fzdcel  10337  fzen  10340  uzsubsubfz  10344  fzrevral2  10403  fzshftral  10405  fz0fzdiffz0  10427  difelfznle  10432  fzo1fzo0n0  10485  fzonmapblen  10489  fzosubel2  10503  ubmelfzo  10508  elfzodifsumelfzo  10509  ssfzo12bi  10533  ubmelm1fzo  10534  subfzo0  10551  ceiqle  10638  modqid2  10676  zmodidfzoimp  10679  addmodidr  10698  modfzo0difsn  10720  addmodlteq  10723  frec2uzf1od  10731  exprecap  10905  expdivap  10915  expubnd  10921  sqdivap  10928  mulbinom2  10981  bernneq2  10986  mulsubdivbinom2ap  11036  bcval3  11076  bccmpl  11079  omgadd  11128  ccatval1  11240  ccatval2  11241  ccatass  11251  lswccatn0lsw  11254  ccatws1lenp1bg  11278  ccatw2s1leng  11281  pfxfv  11331  pfxnd  11336  pfxtrcfv  11340  pfxsuffeqwrdeq  11345  swrdswrd  11352  pfxpfx  11355  ccatopth2  11364  pfxccatin12lem4  11373  pfxccatin12lem1  11375  pfxccatin12lem2  11378  pfxccatin12lem3  11379  pfxccatin12  11380  pfxccat3  11381  swrdccat  11382  pfxccatpfx1  11383  pfxccatpfx2  11384  s3fv0g  11438  s3fv1g  11439  s3fv2g  11440  shftval2  11466  mulreap  11504  elicc4abs  11734  abssubge0  11742  abssuble0  11743  maxleast  11853  maxltsup  11858  xrmaxltsup  11898  xrmineqinf  11909  xrltmininf  11910  xrlemininf  11911  fsumdifsnconst  12096  prodfap0  12186  prodfrecap  12187  fprodabs  12257  sin01gt0  12403  cos01gt0  12404  sin02gt0  12405  dvdscmul  12459  summodnegmod  12463  modmulconst  12464  dvdsleabs  12486  dvdsleabs2  12487  addmodlteqALT  12500  dvdsexp  12502  mulmoddvds  12504  divalgb  12566  divgcdz  12622  gcdass  12666  mulgcdr  12669  gcddiv  12670  uzwodc  12688  lcmass  12737  coprmdvds  12744  qredeq  12748  qredeu  12749  congr  12752  divgcdcoprm0  12753  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  isprm3  12770  dvdsnprmd  12777  euclemma  12798  prmdvdsexpb  12801  prmexpb  12803  rpexp  12805  znege1  12830  modprminv  12902  modprminveq  12903  vfermltl  12904  modprm0  12907  modprmn0modprm0  12909  coprimeprodsq  12910  coprimeprodsq2  12911  pythagtriplem1  12918  pythagtriplem3  12920  pythagtriplem6  12923  pythagtriplem12  12928  pythagtriplem13  12929  pythagtriplem14  12930  pythagtriplem16  12932  pythagtriplem19  12935  pythagtrip  12936  pcmul  12954  pcdiv  12955  pcqcl  12959  pcgcd1  12981  pcgcd  12982  dvdsprmpweq  12988  difsqpwdvds  12991  pcfaclem  13002  unbendc  13155  strle3g  13271  ercpbl  13494  grpinvid1  13715  grpinvid2  13716  grpasscan1  13726  grpasscan2  13727  grpidrcan  13728  grpidlcan  13729  grpinvadd  13741  grpsubadd  13751  grppncan  13754  pwsinvg  13775  qussub  13904  subcmnd  14000  mulgass2  14152  dvrcan1  14235  dvrcan3  14236  rmodislmodlem  14446  rmodislmod  14447  islssm  14453  lsselg  14457  lspss  14495  lspssp  14499  lsslsp  14525  islidlm  14575  lidlnegcl  14581  lidlsubcl  14583  zndvds  14745  basgen  14891  clsss  14929  ntrin  14935  ntrcls0  14942  neiint  14956  neiss  14961  neipsm  14965  opnssneib  14967  innei  14974  restco  14985  iscnp  15010  cnconst2  15044  txcn  15086  psmetsym  15140  psmetlecl  15145  distspace  15146  xmetlecl  15178  xmetsym  15179  xblcntrps  15224  xblcntr  15225  blssec  15249  blpnfctr  15250  txmetcn  15330  cnmet  15341  dvid  15506  dvidre  15508  dvply1  15576  ptolemy  15635  sinq12gt0  15641  sincosq1eq  15650  rpcxpsub  15719  relogbexpap  15769  logbleb  15772  logblt  15773  rplogbcxp  15774  lgsval4  15839  lgsmod  15845  lgsne0  15857  lgsmulsqcoprm  15865  2lgsoddprmlem1  15924  structiedg0val  15981  lpvtx  16020  upgredg2vtx  16089  upgredgpr  16090  ushgredgedg  16167  ushgredgedgloop  16169  usgr2v1e2w  16187  wlkeq  16295  clwwlkccatlem  16341  clwwlkccat  16342  clwwlkext2edg  16363  clwwlknccat  16364  s2elclwwlknon2  16377  clwwlknonex2lem2  16379  repiecele0  16758  repiecege0  16759