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  4464  sotricim  4468  soinxp  4845  funopg  5411  fnco  5491  resasplitss  5569  resdif  5661  fnimapr  5763  ftpg  5899  fsnunfv  5916  fvpr1g  5921  fvpr2g  5922  f1ocnvfvb  5986  f1oiso2  6033  moriotass  6069  f1ofveu  6073  acexmid  6084  ovig  6210  ov6g  6227  ovg  6228  ot1stg  6386  ot2ndg  6387  poxp  6468  suppvalfn  6481  suppsnopdc  6490  suppfnss  6497  funsssuppss  6498  brtposg  6525  smores3  6564  smoiso  6573  rdgivallem  6652  frecsuclem  6677  nnaord  6782  nnaword  6784  nnawordex  6802  ecopovtrn  6906  ecopovtrng  6909  xpdom3m  7132  mapxpen  7148  sbthlemi4  7277  djuenun  7568  netap  7620  2omotaplemap  7623  ltsopi  7687  addcanpig  7701  distrnqg  7754  ltsonq  7765  ltanqg  7767  ltmnqg  7768  nnanq0  7825  distrnq0  7826  distnq0r  7830  prarloclem  7868  genpassl  7891  genpassu  7892  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  1idprl  7957  1idpru  7958  ltpopr  7962  ltsopr  7963  ltexprlemm  7967  ltexprlemfl  7976  ltexprlemfu  7978  addcanprlemu  7982  recexprlem1ssl  8000  recexprlem1ssu  8001  aptipr  8008  lttrsr  8129  ltsosr  8131  ltasrg  8137  recexgt0sr  8140  mulextsr1  8148  axmulass  8240  ltxrlt  8391  axltwlin  8393  axlttrn  8394  axltadd  8395  letr  8408  mul12  8455  add12  8484  subadd  8529  addsub  8537  npncan  8547  nppcan  8548  nnpcan  8549  nppcan3  8550  pnpcan  8565  pnncan  8567  ppncan  8568  subdi  8712  ltaddsub2  8765  leaddsub2  8767  ltaddsublt  8899  apreap  8915  lemul1  8921  reapmul1lem  8922  reapadd1  8924  reapcotr  8926  receuap  8999  divassap  9020  div23ap  9021  divmulassap  9025  divmulasscomap  9026  divcanap4  9029  divsubdirap  9038  divcanap5  9044  divdiv32ap  9050  divdivap2  9054  div2subap  9167  letrp1  9178  ltmulgt12  9195  lediv1  9199  ltdiv2  9217  lediv2  9221  lbinfle  9280  indfdc  9298  indfval  9299  difgtsumgt  9714  xrletr  10210  xrre2  10223  xaddass  10271  ixxdisj  10305  ubioc1  10331  lbico1  10332  elioo5  10335  iccsupr  10368  lbicc2  10386  ubicc2  10387  iccneg  10391  icoshft  10392  icodisj  10394  lincmble  10406  iccf1o  10407  iccen  10409  zltaddlt1le  10410  fztri3or  10443  fzdcel  10444  fzen  10447  uzsubsubfz  10452  fzrevral2  10513  fzshftral  10515  fz0fzdiffz0  10537  difelfznle  10542  fzo1fzo0n0  10595  fzonmapblen  10599  fzosubel2  10613  ubmelfzo  10618  elfzodifsumelfzo  10619  ssfzo12bi  10643  ubmelm1fzo  10644  subfzo0  10661  ceiqle  10750  modqid2  10788  zmodidfzoimp  10791  addmodidr  10810  modfzo0difsn  10832  addmodlteq  10835  frec2uzf1od  10843  exprecap  11017  expdivap  11027  expubnd  11033  sqdivap  11040  mulbinom2  11093  bernneq2  11099  mulsubdivbinom2ap  11149  bcval3  11189  bccmpl  11192  omgadd  11242  ccatval1  11365  ccatval2  11366  ccatass  11376  lswccatn0lsw  11379  ccatws1lenp1bg  11403  ccatw2s1leng  11406  pfxfv  11456  pfxnd  11461  pfxtrcfv  11465  pfxsuffeqwrdeq  11470  swrdswrd  11477  pfxpfx  11480  ccatopth2  11489  pfxccatin12lem4  11498  pfxccatin12lem1  11500  pfxccatin12lem2  11503  pfxccatin12lem3  11504  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  pfxccatpfx1  11508  pfxccatpfx2  11509  s3fv0g  11563  s3fv1g  11564  s3fv2g  11565  shftval2  11591  mulreap  11629  elicc4abs  11860  abssubge0  11868  abssuble0  11869  maxleast  11979  maxltsup  11984  xrmaxltsup  12024  xrmineqinf  12035  xrltmininf  12036  xrlemininf  12037  fsumdifsnconst  12222  prodfap0  12312  prodfrecap  12313  fprodabs  12383  sin01gt0  12529  cos01gt0  12530  sin02gt0  12531  dvdscmul  12585  summodnegmod  12589  modmulconst  12590  dvdsleabs  12612  dvdsleabs2  12613  addmodlteqALT  12626  dvdsexp  12628  mulmoddvds  12630  divalgb  12692  divgcdz  12748  gcdass  12792  mulgcdr  12795  gcddiv  12796  uzwodc  12814  lcmass  12863  coprmdvds  12870  qredeq  12874  qredeu  12875  congr  12878  divgcdcoprm0  12879  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  isprm3  12896  dvdsnprmd  12903  euclemma  12924  prmdvdsexpb  12927  prmexpb  12929  rpexp  12931  znege1  12956  modprminv  13028  modprminveq  13029  vfermltl  13030  modprm0  13033  modprmn0modprm0  13035  coprimeprodsq  13036  coprimeprodsq2  13037  pythagtriplem1  13044  pythagtriplem3  13046  pythagtriplem6  13049  pythagtriplem12  13054  pythagtriplem13  13055  pythagtriplem14  13056  pythagtriplem16  13058  pythagtriplem19  13061  pythagtrip  13062  pcmul  13080  pcdiv  13081  pcqcl  13085  pcgcd1  13107  pcgcd  13108  dvdsprmpweq  13114  difsqpwdvds  13117  pcfaclem  13128  ballotfilemsgt1  13254  ballotfilemrv1  13264  ballotfilemrv2  13265  ballotfilemfrcn0  13273  unbendc  13345  strle3g  13462  ercpbl  13652  grpinvid1  13857  grpinvid2  13858  grpasscan1  13868  grpasscan2  13869  grpidrcan  13870  grpidlcan  13871  grpinvadd  13883  grpsubadd  13893  grppncan  13896  qussub  14040  subcmnd  14137  pwsinvg  14215  rng1zrlem  14258  mulgass2  14363  dvrcan1  14447  dvrcan3  14448  rmodislmodlem  14687  rmodislmod  14688  islssm  14694  lsselg  14698  lspss  14736  lspssp  14740  lsslsp  14766  islidlm  14816  lidlnegcl  14822  lidlsubcl  14824  zndvds  14984  assa2ass  15009  assa2ass2  15010  aspss  15019  basgen  15181  clsss  15219  ntrin  15225  ntrcls0  15232  neiint  15246  neiss  15251  neipsm  15255  opnssneib  15257  innei  15264  restco  15275  iscnp  15300  cnconst2  15334  txcn  15376  psmetsym  15430  psmetlecl  15435  distspace  15436  xmetlecl  15468  xmetsym  15469  xblcntrps  15514  xblcntr  15515  blssec  15539  blpnfctr  15540  txmetcn  15620  cnmet  15631  dvid  15796  dvidre  15798  dvply1  15866  ptolemy  15925  sinq12gt0  15931  sincosq1eq  15940  rpcxpsub  16010  relogbexpap  16060  logbleb  16063  logblt  16064  rplogbcxp  16065  lgsval4  16139  lgsmod  16145  lgsne0  16157  lgsmulsqcoprm  16165  2lgsoddprmlem1  16224  structiedg0val  16281  lpvtx  16320  upgredg2vtx  16389  upgredgpr  16390  ushgredgedg  16467  ushgredgedgloop  16469  usgr2v1e2w  16487  wlkeq  16595  clwwlkccatlem  16641  clwwlkccat  16642  clwwlkext2edg  16663  clwwlknccat  16664  s2elclwwlknon2  16677  clwwlknonex2lem2  16679  repiecele0  17075  repiecege0  17076