Theorem 3adant3 1012

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 989	. 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 103   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  stoic4a  1425  stoic4b  1426  vtoclgft  2780  eqeu  2900  tpssi  3746  issod  4304  sotricim  4308  soinxp  4681  funopg  5232  fnco  5306  resasplitss  5377  resdif  5464  fnimapr  5556  ftpg  5680  fsnunfv  5697  fvpr1g  5702  fvpr2g  5703  f1ocnvfvb  5759  f1oiso2  5806  moriotass  5837  f1ofveu  5841  acexmid  5852  ovig  5974  ov6g  5990  ovg  5991  ot1stg  6131  ot2ndg  6132  poxp  6211  brtposg  6233  smores3  6272  smoiso  6281  rdgivallem  6360  frecsuclem  6385  nnaord  6488  nnaword  6490  nnawordex  6508  ecopovtrn  6610  ecopovtrng  6613  xpdom3m  6812  mapxpen  6826  sbthlemi4  6937  djuenun  7189  ltsopi  7282  addcanpig  7296  distrnqg  7349  ltsonq  7360  ltanqg  7362  ltmnqg  7363  nnanq0  7420  distrnq0  7421  distnq0r  7425  prarloclem  7463  genpassl  7486  genpassu  7487  distrlem1prl  7544  distrlem1pru  7545  distrlem5prl  7548  distrlem5pru  7549  1idprl  7552  1idpru  7553  ltpopr  7557  ltsopr  7558  ltexprlemm  7562  ltexprlemfl  7571  ltexprlemfu  7573  addcanprlemu  7577  recexprlem1ssl  7595  recexprlem1ssu  7596  aptipr  7603  lttrsr  7724  ltsosr  7726  ltasrg  7732  recexgt0sr  7735  mulextsr1  7743  axmulass  7835  ltxrlt  7985  axltwlin  7987  axlttrn  7988  axltadd  7989  letr  8002  mul12  8048  add12  8077  subadd  8122  addsub  8130  npncan  8140  nppcan  8141  nnpcan  8142  nppcan3  8143  pnpcan  8158  pnncan  8160  ppncan  8161  subdi  8304  ltaddsub2  8356  leaddsub2  8358  ltaddsublt  8490  apreap  8506  lemul1  8512  reapmul1lem  8513  reapadd1  8515  reapcotr  8517  receuap  8587  divassap  8607  div23ap  8608  divmulassap  8612  divmulasscomap  8613  divcanap4  8616  divsubdirap  8625  divcanap5  8631  divdiv32ap  8637  divdivap2  8641  div2subap  8754  letrp1  8764  ltmulgt12  8781  lediv1  8785  ltdiv2  8803  lediv2  8807  lbinfle  8866  difgtsumgt  9281  xrletr  9765  xrre2  9778  xaddass  9826  ixxdisj  9860  ubioc1  9886  lbico1  9887  elioo5  9890  iccsupr  9923  lbicc2  9941  ubicc2  9942  iccneg  9946  icoshft  9947  icodisj  9949  iccf1o  9961  iccen  9963  zltaddlt1le  9964  fztri3or  9995  fzdcel  9996  fzen  9999  uzsubsubfz  10003  fzrevral2  10062  fzshftral  10064  fz0fzdiffz0  10086  difelfznle  10091  fzo1fzo0n0  10139  fzonmapblen  10143  fzosubel2  10151  ubmelfzo  10156  elfzodifsumelfzo  10157  ssfzo12bi  10181  ubmelm1fzo  10182  subfzo0  10198  ceiqle  10269  modqid2  10307  zmodidfzoimp  10310  addmodidr  10329  modfzo0difsn  10351  addmodlteq  10354  frec2uzf1od  10362  exprecap  10517  expdivap  10527  expubnd  10533  sqdivap  10540  mulbinom2  10592  bernneq2  10597  bcval3  10685  bccmpl  10688  omgadd  10737  shftval2  10790  mulreap  10828  elicc4abs  11058  abssubge0  11066  abssuble0  11067  maxleast  11177  maxltsup  11182  xrmaxltsup  11221  xrmineqinf  11232  xrltmininf  11233  xrlemininf  11234  fsumdifsnconst  11418  prodfap0  11508  prodfrecap  11509  fprodabs  11579  sin01gt0  11724  cos01gt0  11725  sin02gt0  11726  dvdscmul  11780  summodnegmod  11784  modmulconst  11785  dvdsleabs  11805  dvdsleabs2  11806  addmodlteqALT  11819  dvdsexp  11821  mulmoddvds  11823  divalgb  11884  divgcdz  11926  gcdass  11970  mulgcdr  11973  gcddiv  11974  uzwodc  11992  lcmass  12039  coprmdvds  12046  qredeq  12050  qredeu  12051  congr  12054  divgcdcoprm0  12055  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  isprm3  12072  dvdsnprmd  12079  euclemma  12100  prmdvdsexpb  12103  prmexpb  12105  rpexp  12107  znege1  12132  modprminv  12203  modprminveq  12204  vfermltl  12205  modprm0  12208  modprmn0modprm0  12210  coprimeprodsq  12211  coprimeprodsq2  12212  pythagtriplem1  12219  pythagtriplem3  12221  pythagtriplem6  12224  pythagtriplem12  12229  pythagtriplem13  12230  pythagtriplem14  12231  pythagtriplem16  12233  pythagtriplem19  12236  pythagtrip  12237  pcmul  12255  pcdiv  12256  pcqcl  12260  pcgcd1  12281  pcgcd  12282  dvdsprmpweq  12288  difsqpwdvds  12291  pcfaclem  12301  unbendc  12409  strle3g  12510  grpinvid1  12754  grpinvid2  12755  grpasscan1  12762  grpasscan2  12763  grpidrcan  12764  grpidlcan  12765  basgen  12874  clsss  12912  ntrin  12918  ntrcls0  12925  neiint  12939  neiss  12944  neipsm  12948  opnssneib  12950  innei  12957  restco  12968  iscnp  12993  cnconst2  13027  txcn  13069  psmetsym  13123  psmetlecl  13128  distspace  13129  xmetlecl  13161  xmetsym  13162  xblcntrps  13207  xblcntr  13208  blssec  13232  blpnfctr  13233  txmetcn  13313  cnmet  13324  dvid  13456  ptolemy  13539  sinq12gt0  13545  sincosq1eq  13554  rpcxpsub  13623  relogbexpap  13670  logbleb  13673  logblt  13674  rplogbcxp  13675  lgsval4  13715  lgsmod  13721  lgsne0  13733  lgsmulsqcoprm  13741