Theorem 3adant3 1019

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 996	. 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 980

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 982

This theorem is referenced by:  stoic4a  1443  stoic4b  1444  vtoclgft  2802  eqeu  2922  tpssi  3774  issod  4337  sotricim  4341  soinxp  4714  funopg  5269  fnco  5343  resasplitss  5414  resdif  5502  fnimapr  5597  ftpg  5721  fsnunfv  5738  fvpr1g  5743  fvpr2g  5744  f1ocnvfvb  5802  f1oiso2  5849  moriotass  5881  f1ofveu  5885  acexmid  5896  ovig  6019  ov6g  6035  ovg  6036  ot1stg  6178  ot2ndg  6179  poxp  6258  brtposg  6280  smores3  6319  smoiso  6328  rdgivallem  6407  frecsuclem  6432  nnaord  6535  nnaword  6537  nnawordex  6555  ecopovtrn  6659  ecopovtrng  6662  xpdom3m  6861  mapxpen  6877  sbthlemi4  6990  djuenun  7242  netap  7284  2omotaplemap  7287  ltsopi  7350  addcanpig  7364  distrnqg  7417  ltsonq  7428  ltanqg  7430  ltmnqg  7431  nnanq0  7488  distrnq0  7489  distnq0r  7493  prarloclem  7531  genpassl  7554  genpassu  7555  distrlem1prl  7612  distrlem1pru  7613  distrlem5prl  7616  distrlem5pru  7617  1idprl  7620  1idpru  7621  ltpopr  7625  ltsopr  7626  ltexprlemm  7630  ltexprlemfl  7639  ltexprlemfu  7641  addcanprlemu  7645  recexprlem1ssl  7663  recexprlem1ssu  7664  aptipr  7671  lttrsr  7792  ltsosr  7794  ltasrg  7800  recexgt0sr  7803  mulextsr1  7811  axmulass  7903  ltxrlt  8054  axltwlin  8056  axlttrn  8057  axltadd  8058  letr  8071  mul12  8117  add12  8146  subadd  8191  addsub  8199  npncan  8209  nppcan  8210  nnpcan  8211  nppcan3  8212  pnpcan  8227  pnncan  8229  ppncan  8230  subdi  8373  ltaddsub2  8425  leaddsub2  8427  ltaddsublt  8559  apreap  8575  lemul1  8581  reapmul1lem  8582  reapadd1  8584  reapcotr  8586  receuap  8657  divassap  8678  div23ap  8679  divmulassap  8683  divmulasscomap  8684  divcanap4  8687  divsubdirap  8696  divcanap5  8702  divdiv32ap  8708  divdivap2  8712  div2subap  8825  letrp1  8836  ltmulgt12  8853  lediv1  8857  ltdiv2  8875  lediv2  8879  lbinfle  8938  difgtsumgt  9353  xrletr  9840  xrre2  9853  xaddass  9901  ixxdisj  9935  ubioc1  9961  lbico1  9962  elioo5  9965  iccsupr  9998  lbicc2  10016  ubicc2  10017  iccneg  10021  icoshft  10022  icodisj  10024  iccf1o  10036  iccen  10038  zltaddlt1le  10039  fztri3or  10071  fzdcel  10072  fzen  10075  uzsubsubfz  10079  fzrevral2  10138  fzshftral  10140  fz0fzdiffz0  10162  difelfznle  10167  fzo1fzo0n0  10215  fzonmapblen  10219  fzosubel2  10227  ubmelfzo  10232  elfzodifsumelfzo  10233  ssfzo12bi  10257  ubmelm1fzo  10258  subfzo0  10274  ceiqle  10346  modqid2  10384  zmodidfzoimp  10387  addmodidr  10406  modfzo0difsn  10428  addmodlteq  10431  frec2uzf1od  10439  exprecap  10595  expdivap  10605  expubnd  10611  sqdivap  10618  mulbinom2  10671  bernneq2  10676  mulsubdivbinom2ap  10726  bcval3  10766  bccmpl  10769  omgadd  10817  shftval2  10870  mulreap  10908  elicc4abs  11138  abssubge0  11146  abssuble0  11147  maxleast  11257  maxltsup  11262  xrmaxltsup  11301  xrmineqinf  11312  xrltmininf  11313  xrlemininf  11314  fsumdifsnconst  11498  prodfap0  11588  prodfrecap  11589  fprodabs  11659  sin01gt0  11804  cos01gt0  11805  sin02gt0  11806  dvdscmul  11860  summodnegmod  11864  modmulconst  11865  dvdsleabs  11886  dvdsleabs2  11887  addmodlteqALT  11900  dvdsexp  11902  mulmoddvds  11904  divalgb  11965  divgcdz  12007  gcdass  12051  mulgcdr  12054  gcddiv  12055  uzwodc  12073  lcmass  12120  coprmdvds  12127  qredeq  12131  qredeu  12132  congr  12135  divgcdcoprm0  12136  divgcdcoprmex  12137  cncongr1  12138  cncongr2  12139  isprm3  12153  dvdsnprmd  12160  euclemma  12181  prmdvdsexpb  12184  prmexpb  12186  rpexp  12188  znege1  12213  modprminv  12284  modprminveq  12285  vfermltl  12286  modprm0  12289  modprmn0modprm0  12291  coprimeprodsq  12292  coprimeprodsq2  12293  pythagtriplem1  12300  pythagtriplem3  12302  pythagtriplem6  12305  pythagtriplem12  12310  pythagtriplem13  12311  pythagtriplem14  12312  pythagtriplem16  12314  pythagtriplem19  12317  pythagtrip  12318  pcmul  12336  pcdiv  12337  pcqcl  12341  pcgcd1  12363  pcgcd  12364  dvdsprmpweq  12370  difsqpwdvds  12373  pcfaclem  12384  unbendc  12508  strle3g  12623  ercpbl  12810  grpinvid1  13011  grpinvid2  13012  grpasscan1  13022  grpasscan2  13023  grpidrcan  13024  grpidlcan  13025  grpinvadd  13037  grpsubadd  13047  grppncan  13050  qussub  13193  subcmnd  13287  mulgass2  13427  dvrcan1  13507  dvrcan3  13508  rmodislmodlem  13683  rmodislmod  13684  islssm  13690  lsselg  13694  lspss  13732  lspssp  13736  lsslsp  13762  islidlm  13812  lidlnegcl  13818  lidlsubcl  13820  basgen  14057  clsss  14095  ntrin  14101  ntrcls0  14108  neiint  14122  neiss  14127  neipsm  14131  opnssneib  14133  innei  14140  restco  14151  iscnp  14176  cnconst2  14210  txcn  14252  psmetsym  14306  psmetlecl  14311  distspace  14312  xmetlecl  14344  xmetsym  14345  xblcntrps  14390  xblcntr  14391  blssec  14415  blpnfctr  14416  txmetcn  14496  cnmet  14507  dvid  14639  ptolemy  14722  sinq12gt0  14728  sincosq1eq  14737  rpcxpsub  14806  relogbexpap  14853  logbleb  14856  logblt  14857  rplogbcxp  14858  lgsval4  14899  lgsmod  14905  lgsne0  14917  lgsmulsqcoprm  14925  2lgsoddprmlem1  14931