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  4366  sotricim  4370  soinxp  4745  funopg  5305  fnco  5384  resasplitss  5455  resdif  5544  fnimapr  5639  ftpg  5768  fsnunfv  5785  fvpr1g  5790  fvpr2g  5791  f1ocnvfvb  5849  f1oiso2  5896  moriotass  5928  f1ofveu  5932  acexmid  5943  ovig  6067  ov6g  6084  ovg  6085  ot1stg  6238  ot2ndg  6239  poxp  6318  brtposg  6340  smores3  6379  smoiso  6388  rdgivallem  6467  frecsuclem  6492  nnaord  6595  nnaword  6597  nnawordex  6615  ecopovtrn  6719  ecopovtrng  6722  xpdom3m  6929  mapxpen  6945  sbthlemi4  7062  djuenun  7324  netap  7366  2omotaplemap  7369  ltsopi  7433  addcanpig  7447  distrnqg  7500  ltsonq  7511  ltanqg  7513  ltmnqg  7514  nnanq0  7571  distrnq0  7572  distnq0r  7576  prarloclem  7614  genpassl  7637  genpassu  7638  distrlem1prl  7695  distrlem1pru  7696  distrlem5prl  7699  distrlem5pru  7700  1idprl  7703  1idpru  7704  ltpopr  7708  ltsopr  7709  ltexprlemm  7713  ltexprlemfl  7722  ltexprlemfu  7724  addcanprlemu  7728  recexprlem1ssl  7746  recexprlem1ssu  7747  aptipr  7754  lttrsr  7875  ltsosr  7877  ltasrg  7883  recexgt0sr  7886  mulextsr1  7894  axmulass  7986  ltxrlt  8138  axltwlin  8140  axlttrn  8141  axltadd  8142  letr  8155  mul12  8201  add12  8230  subadd  8275  addsub  8283  npncan  8293  nppcan  8294  nnpcan  8295  nppcan3  8296  pnpcan  8311  pnncan  8313  ppncan  8314  subdi  8457  ltaddsub2  8510  leaddsub2  8512  ltaddsublt  8644  apreap  8660  lemul1  8666  reapmul1lem  8667  reapadd1  8669  reapcotr  8671  receuap  8742  divassap  8763  div23ap  8764  divmulassap  8768  divmulasscomap  8769  divcanap4  8772  divsubdirap  8781  divcanap5  8787  divdiv32ap  8793  divdivap2  8797  div2subap  8910  letrp1  8921  ltmulgt12  8938  lediv1  8942  ltdiv2  8960  lediv2  8964  lbinfle  9023  difgtsumgt  9442  xrletr  9930  xrre2  9943  xaddass  9991  ixxdisj  10025  ubioc1  10051  lbico1  10052  elioo5  10055  iccsupr  10088  lbicc2  10106  ubicc2  10107  iccneg  10111  icoshft  10112  icodisj  10114  iccf1o  10126  iccen  10128  zltaddlt1le  10129  fztri3or  10161  fzdcel  10162  fzen  10165  uzsubsubfz  10169  fzrevral2  10228  fzshftral  10230  fz0fzdiffz0  10252  difelfznle  10257  fzo1fzo0n0  10307  fzonmapblen  10311  fzosubel2  10324  ubmelfzo  10329  elfzodifsumelfzo  10330  ssfzo12bi  10354  ubmelm1fzo  10355  subfzo0  10371  ceiqle  10458  modqid2  10496  zmodidfzoimp  10499  addmodidr  10518  modfzo0difsn  10540  addmodlteq  10543  frec2uzf1od  10551  exprecap  10725  expdivap  10735  expubnd  10741  sqdivap  10748  mulbinom2  10801  bernneq2  10806  mulsubdivbinom2ap  10856  bcval3  10896  bccmpl  10899  omgadd  10947  ccatval1  11053  ccatval2  11054  ccatass  11064  lswccatn0lsw  11067  ccatws1lenp1bg  11089  shftval2  11137  mulreap  11175  elicc4abs  11405  abssubge0  11413  abssuble0  11414  maxleast  11524  maxltsup  11529  xrmaxltsup  11569  xrmineqinf  11580  xrltmininf  11581  xrlemininf  11582  fsumdifsnconst  11766  prodfap0  11856  prodfrecap  11857  fprodabs  11927  sin01gt0  12073  cos01gt0  12074  sin02gt0  12075  dvdscmul  12129  summodnegmod  12133  modmulconst  12134  dvdsleabs  12156  dvdsleabs2  12157  addmodlteqALT  12170  dvdsexp  12172  mulmoddvds  12174  divalgb  12236  divgcdz  12292  gcdass  12336  mulgcdr  12339  gcddiv  12340  uzwodc  12358  lcmass  12407  coprmdvds  12414  qredeq  12418  qredeu  12419  congr  12422  divgcdcoprm0  12423  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  isprm3  12440  dvdsnprmd  12447  euclemma  12468  prmdvdsexpb  12471  prmexpb  12473  rpexp  12475  znege1  12500  modprminv  12572  modprminveq  12573  vfermltl  12574  modprm0  12577  modprmn0modprm0  12579  coprimeprodsq  12580  coprimeprodsq2  12581  pythagtriplem1  12588  pythagtriplem3  12590  pythagtriplem6  12593  pythagtriplem12  12598  pythagtriplem13  12599  pythagtriplem14  12600  pythagtriplem16  12602  pythagtriplem19  12605  pythagtrip  12606  pcmul  12624  pcdiv  12625  pcqcl  12629  pcgcd1  12651  pcgcd  12652  dvdsprmpweq  12658  difsqpwdvds  12661  pcfaclem  12672  unbendc  12825  strle3g  12940  ercpbl  13163  grpinvid1  13384  grpinvid2  13385  grpasscan1  13395  grpasscan2  13396  grpidrcan  13397  grpidlcan  13398  grpinvadd  13410  grpsubadd  13420  grppncan  13423  pwsinvg  13444  qussub  13573  subcmnd  13669  mulgass2  13820  dvrcan1  13902  dvrcan3  13903  rmodislmodlem  14112  rmodislmod  14113  islssm  14119  lsselg  14123  lspss  14161  lspssp  14165  lsslsp  14191  islidlm  14241  lidlnegcl  14247  lidlsubcl  14249  zndvds  14411  basgen  14552  clsss  14590  ntrin  14596  ntrcls0  14603  neiint  14617  neiss  14622  neipsm  14626  opnssneib  14628  innei  14635  restco  14646  iscnp  14671  cnconst2  14705  txcn  14747  psmetsym  14801  psmetlecl  14806  distspace  14807  xmetlecl  14839  xmetsym  14840  xblcntrps  14885  xblcntr  14886  blssec  14910  blpnfctr  14911  txmetcn  14991  cnmet  15002  dvid  15167  dvidre  15169  dvply1  15237  ptolemy  15296  sinq12gt0  15302  sincosq1eq  15311  rpcxpsub  15380  relogbexpap  15430  logbleb  15433  logblt  15434  rplogbcxp  15435  lgsval4  15497  lgsmod  15503  lgsne0  15515  lgsmulsqcoprm  15523  2lgsoddprmlem1  15582  structiedg0val  15637