Theorem 3adant2 1043

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
3adant2	|- ( ( ph /\ th /\ ps ) -> ch )

Proof of Theorem 3adant2

Step	Hyp	Ref	Expression
1		3simpb 1022	. 2 |- ( ( ph /\ th /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( ph /\ th /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3ad2ant1  1045  3imp3i2an  1210  eupickb  2162  vtoclegft  2889  eqeu  2987  ifnebibdc  3668  suc11g  4679  soinxp  4820  funopg  5386  fnco  5466  dff1o2  5619  fnimapr  5737  fvun1  5743  fvmptt  5769  fnreseql  5788  fvpr1g  5890  fvpr2g  5891  f1elima  5946  f1ocnvfvb  5953  ovexg  6084  oprssov  6196  poxp  6428  smoiso  6533  rdgivallem  6612  nndi  6719  nndir  6723  fnsnsplitdc  6738  nnaord  6742  nnaordr  6743  nnaword  6744  nnawordi  6748  ecopovtrn  6866  ecopovtrng  6869  mapsnd  6923  xpdom3m  7085  mapxpen  7101  findcard  7145  fisseneq  7195  resfnfinfinss  7206  funrnfi  7209  netap  7568  2omotaplemap  7571  ltsopi  7635  addcanpig  7649  addassnqg  7697  distrnqg  7702  ltsonq  7713  ltmnqg  7716  prarloclemarch2  7734  nnanq0  7773  distrnq0  7774  distnq0r  7778  prltlu  7802  prarloclem5  7815  distrlem1prl  7897  distrlem1pru  7898  distrlem5prl  7901  distrlem5pru  7902  ltpopr  7910  ltsopr  7911  ltexprlemm  7915  ltexprlemfl  7924  ltexprlemfu  7926  lttrsr  8077  ltsosr  8079  ltasrg  8085  recexgt0sr  8088  mulextsr1lem  8095  mulextsr1  8096  axpre-mulext  8203  adddir  8265  axltwlin  8341  axlttrn  8342  ltleletr  8355  letr  8356  nnncan1  8509  npncan3  8511  pnpcan2  8513  subdi  8658  subdir  8659  reapcotr  8872  divmulap  8949  div23ap  8965  div13ap  8967  muldivdirap  8981  divsubdirap  8982  divcanap7  8995  ltmul2  9130  lemul2  9131  lemul2a  9133  lediv1  9143  ltmuldiv2  9149  lemuldiv2  9156  squeeze0  9178  nndivtr  9279  bndndx  9495  nn0n0n1ge2  9648  fnn0ind  9694  addlelt  10101  xrletr  10141  xrltne  10146  xleadd2a  10207  xleadd1  10208  xltadd2  10210  iooneg  10321  iccneg  10322  icoshft  10323  icoshftf1o  10324  zltaddlt1le  10341  fztri3or  10373  fzdcel  10374  fzen  10377  uzsubsubfz  10381  fzrevral2  10440  fzshftral  10442  fz0fzdiffz0  10464  elfzmlbp  10466  elfzo  10483  nelfzo  10486  fzoaddel2  10535  fzosubel2  10540  elfzom1p1elfzo  10559  ssfzo12bi  10570  subfzo0  10588  flltdivnn0lt  10664  modqmulnn  10704  modfzo0difsn  10757  expdivap  10952  expubnd  10958  mulbinom2  11018  bernneq2  11023  ccatval1  11285  ccatval3  11287  ccatfv0  11291  ccatval1lsw  11292  ccatws1lenp1bg  11323  pfxsuffeqwrdeq  11390  pfxsuff1eqwrdeq  11391  swrdswrd  11397  pfxpfx  11400  wrd2ind  11415  swrdccatin1  11417  pfxccatin12lem1  11420  swrdccatin2  11421  pfxccatin12lem3  11424  swrdccat  11427  pfxccatpfx1  11428  pfxccatpfx2  11429  swrdccat3blem  11431  shftuz  11502  shftval2  11511  abs3dif  11790  xrmaxlesup  11944  xrltmininf  11955  xrlemininf  11956  sin02gt0  12450  dvdsval2  12476  dvdscmul  12504  dvdsmulc  12505  ndvdssub  12616  rpmulgcd  12722  cncongr1  12800  cncongr2  12801  isprm3  12815  coprimeprodsq  12955  pythagtriplem12  12973  pythagtriplem14  12975  pcmul  12999  pcdiv  13000  pcqcl  13004  pcqdiv  13005  pcdvdsb  13018  ercpbl  13544  mgmb1mgm1  13581  grpinvid1  13765  grpinvid2  13766  grpasscan1  13776  grpasscan2  13777  grpinvadd  13791  grpsubf  13792  grpsubrcan  13794  grpinvsub  13795  grpsubeq0  13799  grpsubadd0sub  13800  grppncan  13804  grpnpcan  13805  mulgnn0p1  13850  mulgaddcomlem  13862  mulginvcom  13864  mulginvinv  13865  subgsubcl  13902  subgsub  13903  eqglact  13942  quselbasg  13947  quseccl0g  13948  qussub  13954  ghmsub  13968  subcmnd  14050  srg1zr  14131  dvrcl  14280  unitdvcl  14281  dvrcan1  14285  dvrcan3  14286  dvreq1  14287  subrgdv  14383  lmodvsubval2  14490  lmodprop2d  14496  zndvds  14797  ntrin  14989  elnei  15017  cnrest2  15101  psmetsym  15194  psmetge0  15196  xmetge0  15230  xmetsym  15233  cnmet  15395  rpcxpsub  15773  rpdivcxp  15776  logbleb  15826  logblt  15827  lgsmodeq  15918  lgsmulsqcoprm  15919  gausslemma2dlem1a  15931  2lgsoddprmlem2  15979  upgrpredgv  16141  issubgr2  16253  uhgrissubgr  16256  egrsubgr  16258  upgrwlkvtxedg  16359  clwwlk1loop  16394  clwwlkccatlem  16395  clwwlknonex2lem2  16433  bj-peano4  16725