Theorem 3adant3 1048

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 1025	. 2 |- ( ( ph /\ ps /\ th ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( ph /\ ps /\ th ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  stoic4a  1481  stoic4b  1482  vtoclgft  2873  eqeu  2996  ssprsseq  3877  tpssi  3884  issod  4466  sotricim  4470  soinxp  4847  funopg  5414  fnco  5494  resasplitss  5572  resdif  5664  fnimapr  5766  ftpg  5902  fsnunfv  5919  fvpr1g  5924  fvpr2g  5925  f1ocnvfvb  5989  f1oiso2  6036  moriotass  6072  f1ofveu  6076  acexmid  6087  ovig  6213  ov6g  6230  ovg  6231  ot1stg  6390  ot2ndg  6391  poxp  6472  suppvalfn  6485  suppsnopdc  6494  suppfnss  6501  funsssuppss  6502  brtposg  6529  smores3  6568  smoiso  6577  rdgivallem  6656  frecsuclem  6681  nnaord  6786  nnaword  6788  nnawordex  6806  ecopovtrn  6910  ecopovtrng  6913  xpdom3m  7136  mapxpen  7152  sbthlemi4  7282  djuenun  7574  netap  7626  2omotaplemap  7629  ltsopi  7693  addcanpig  7707  distrnqg  7760  ltsonq  7771  ltanqg  7773  ltmnqg  7774  nnanq0  7831  distrnq0  7832  distnq0r  7836  prarloclem  7874  genpassl  7897  genpassu  7898  distrlem1prl  7955  distrlem1pru  7956  distrlem5prl  7959  distrlem5pru  7960  1idprl  7963  1idpru  7964  ltpopr  7968  ltsopr  7969  ltexprlemm  7973  ltexprlemfl  7982  ltexprlemfu  7984  addcanprlemu  7988  recexprlem1ssl  8006  recexprlem1ssu  8007  aptipr  8014  lttrsr  8135  ltsosr  8137  ltasrg  8143  recexgt0sr  8146  mulextsr1  8154  axmulass  8246  ltxrlt  8397  axltwlin  8399  axlttrn  8400  axltadd  8401  letr  8414  mul12  8462  add12  8491  subadd  8536  addsub  8544  npncan  8554  nppcan  8555  nnpcan  8556  nppcan3  8557  pnpcan  8572  pnncan  8574  ppncan  8575  subdi  8719  ltaddsub2  8772  leaddsub2  8774  ltaddsublt  8907  apreap  8923  lemul1  8929  reapmul1lem  8930  reapadd1  8932  reapcotr  8934  receuap  9007  divassap  9028  div23ap  9029  divmulassap  9033  divmulasscomap  9034  divcanap4  9037  divsubdirap  9046  divcanap5  9052  divdiv32ap  9058  divdivap2  9062  div2subap  9175  letrp1  9186  ltmulgt12  9203  lediv1  9207  ltdiv2  9225  lediv2  9229  lbinfle  9288  indfdc  9307  indfval  9308  difgtsumgt  9725  xrletr  10227  xrre2  10240  xaddass  10288  ixxdisj  10322  ubioc1  10348  lbico1  10349  elioo5  10352  iccsupr  10385  lbicc2  10403  ubicc2  10404  iccneg  10408  icoshft  10409  icodisj  10411  lincmble  10423  iccf1o  10424  iccen  10426  zltaddlt1le  10427  fztri3or  10460  fzdcel  10461  fzen  10464  uzsubsubfz  10469  fzrevral2  10530  fzshftral  10532  fz0fzdiffz0  10554  difelfznle  10559  fzo1fzo0n0  10612  fzonmapblen  10616  fzosubel2  10630  ubmelfzo  10635  elfzodifsumelfzo  10636  ssfzo12bi  10660  ubmelm1fzo  10661  subfzo0  10678  ceiqle  10771  modqid2  10809  zmodidfzoimp  10812  addmodidr  10831  modfzo0difsn  10853  addmodlteq  10856  frec2uzf1od  10864  exprecap  11038  expdivap  11048  expubnd  11054  sqdivap  11061  mulbinom2  11114  bernneq2  11120  mulsubdivbinom2ap  11171  bcval3  11211  bccmpl  11214  omgadd  11264  ccatval1  11387  ccatval2  11388  ccatass  11398  lswccatn0lsw  11401  ccatws1lenp1bg  11425  ccatw2s1leng  11428  pfxfv  11478  pfxnd  11483  pfxtrcfv  11487  pfxsuffeqwrdeq  11492  swrdswrd  11499  pfxpfx  11502  ccatopth2  11511  pfxccatin12lem4  11520  pfxccatin12lem1  11522  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  pfxccatpfx1  11530  pfxccatpfx2  11531  s3fv0g  11585  s3fv1g  11586  s3fv2g  11587  shftval2  11613  mulreap  11651  elicc4abs  11883  abssubge0  11891  abssuble0  11892  maxleast  12002  maxltsup  12007  xrmaxltsup  12049  xrmineqinf  12060  xrltmininf  12061  xrlemininf  12062  fsumdifsnconst  12247  prodfap0  12337  prodfrecap  12338  fprodabs  12408  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  dvdscmul  12610  summodnegmod  12614  modmulconst  12615  dvdsleabs  12637  dvdsleabs2  12638  addmodlteqALT  12651  dvdsexp  12653  mulmoddvds  12655  divalgb  12717  divgcdz  12773  gcdass  12817  mulgcdr  12820  gcddiv  12821  uzwodc  12839  lcmass  12888  coprmdvds  12895  qredeq  12899  qredeu  12900  congr  12903  divgcdcoprm0  12904  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  isprm3  12921  dvdsnprmd  12928  euclemma  12950  prmdvdsexpb  12953  prmexpb  12955  rpexp  12957  znege1  12983  modprminv  13057  modprminveq  13058  vfermltl  13059  modprm0  13062  modprmn0modprm0  13064  coprimeprodsq  13065  coprimeprodsq2  13066  pythagtriplem1  13073  pythagtriplem3  13075  pythagtriplem6  13078  pythagtriplem12  13083  pythagtriplem13  13084  pythagtriplem14  13085  pythagtriplem16  13087  pythagtriplem19  13090  pythagtrip  13091  pcmul  13109  pcdiv  13110  pcqcl  13114  pcgcd1  13136  pcgcd  13137  dvdsprmpweq  13143  difsqpwdvds  13146  pcfaclem  13157  ballotfilemsgt1  13312  ballotfilemrv1  13322  ballotfilemrv2  13323  ballotfilemfrcn0  13331  unbendc  13403  strle3g  13521  ercpbl  13711  grpinvid1  13916  grpinvid2  13917  grpasscan1  13927  grpasscan2  13928  grpidrcan  13929  grpidlcan  13930  grpinvadd  13942  grpsubadd  13952  grppncan  13955  qussub  14099  subcmnd  14227  pwsinvg  14322  rng1zrlem  14365  mulgass2  14470  dvrcan1  14556  dvrcan3  14557  rmodislmodlem  14796  rmodislmod  14797  islssm  14803  lsselg  14807  lspss  14845  lspssp  14849  lsslsp  14875  islidlm  14925  lidlnegcl  14931  lidlsubcl  14933  zndvds  15093  assa2ass  15118  assa2ass2  15119  aspss  15128  basgen  15306  clsss  15344  ntrin  15350  ntrcls0  15357  neiint  15371  neiss  15376  neipsm  15380  opnssneib  15382  innei  15389  restco  15400  iscnp  15425  cnconst2  15459  txcn  15501  psmetsym  15555  psmetlecl  15560  distspace  15561  xmetlecl  15593  xmetsym  15594  xblcntrps  15639  xblcntr  15640  blssec  15664  blpnfctr  15665  txmetcn  15745  cnmet  15756  dvid  15921  dvidre  15923  dvply1  15991  ptolemy  16051  sinq12gt0  16057  sincosq1eq  16066  rpcxpsub  16141  relogbexpap  16194  logbleb  16197  logblt  16198  rplogbcxp  16199  lgsval4  16344  lgsmod  16350  lgsne0  16362  lgsmulsqcoprm  16370  2lgsoddprmlem1  16429  structiedg0val  16486  lpvtx  16525  upgredg2vtx  16594  upgredgpr  16595  ushgredgedg  16672  ushgredgedgloop  16674  usgr2v1e2w  16692  wlkeq  16800  clwwlkccatlem  16846  clwwlkccat  16847  clwwlkext2edg  16868  clwwlknccat  16869  s2elclwwlknon2  16882  clwwlknonex2lem2  16884  repiecele0  17281  repiecege0  17282