Theorem 3adant2 1047

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 1026	. 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 1009

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 1011

This theorem is referenced by:  3ad2ant1  1049  3imp3i2an  1214  eupickb  2168  vtoclegft  2897  eqeu  2996  ifnebibdc  3683  suc11g  4699  soinxp  4840  funopg  5406  fnco  5486  dff1o2  5639  fnimapr  5757  fvun1  5763  fvmptt  5791  fnreseql  5810  fvpr1g  5912  fvpr2g  5913  f1elima  5969  f1ocnvfvb  5976  ovexg  6109  oprssov  6221  poxp  6458  smoiso  6563  rdgivallem  6642  nndi  6749  nndir  6753  fnsnsplitdc  6768  nnaord  6772  nnaordr  6773  nnaword  6774  nnawordi  6778  ecopovtrn  6896  ecopovtrng  6899  mapsnd  6960  xpdom3m  7122  mapxpen  7138  findcard  7182  fisseneq  7232  resfnfinfinss  7243  funrnfi  7246  netap  7610  2omotaplemap  7613  ltsopi  7677  addcanpig  7691  addassnqg  7739  distrnqg  7744  ltsonq  7755  ltmnqg  7758  prarloclemarch2  7776  nnanq0  7815  distrnq0  7816  distnq0r  7820  prltlu  7844  prarloclem5  7857  distrlem1prl  7939  distrlem1pru  7940  distrlem5prl  7943  distrlem5pru  7944  ltpopr  7952  ltsopr  7953  ltexprlemm  7957  ltexprlemfl  7966  ltexprlemfu  7968  lttrsr  8119  ltsosr  8121  ltasrg  8127  recexgt0sr  8130  mulextsr1lem  8137  mulextsr1  8138  axpre-mulext  8245  adddir  8307  axltwlin  8383  axlttrn  8384  ltleletr  8397  letr  8398  nnncan1  8552  npncan3  8554  pnpcan2  8556  subdi  8702  subdir  8703  reapcotr  8916  divmulap  8995  div23ap  9011  div13ap  9013  muldivdirap  9027  divsubdirap  9028  divcanap7  9041  ltmul2  9176  lemul2  9177  lemul2a  9179  lediv1  9189  ltmuldiv2  9195  lemuldiv2  9202  squeeze0  9224  nndivtr  9325  bndndx  9541  nn0n0n1ge2  9694  fnn0ind  9741  addlelt  10148  xrletr  10189  xrltne  10194  xleadd2a  10255  xleadd1  10256  xltadd2  10258  iooneg  10369  iccneg  10370  icoshft  10371  icoshftf1o  10372  zltaddlt1le  10389  fztri3or  10422  fzdcel  10423  fzen  10426  uzsubsubfz  10430  fzrevral2  10491  fzshftral  10493  fz0fzdiffz0  10515  elfzmlbp  10517  elfzo  10534  nelfzo  10537  fzoaddel2  10586  fzosubel2  10591  elfzom1p1elfzo  10610  ssfzo12bi  10621  subfzo0  10639  flltdivnn0lt  10717  modqmulnn  10757  modfzo0difsn  10810  expdivap  11005  expubnd  11011  mulbinom2  11071  bernneq2  11077  ccatval1  11343  ccatval3  11345  ccatfv0  11349  ccatval1lsw  11350  ccatws1lenp1bg  11381  pfxsuffeqwrdeq  11448  pfxsuff1eqwrdeq  11449  swrdswrd  11455  pfxpfx  11458  wrd2ind  11473  swrdccatin1  11475  pfxccatin12lem1  11478  swrdccatin2  11479  pfxccatin12lem3  11482  swrdccat  11485  pfxccatpfx1  11486  pfxccatpfx2  11487  swrdccat3blem  11489  shftuz  11560  shftval2  11569  abs3dif  11849  xrmaxlesup  12003  xrltmininf  12014  xrlemininf  12015  sin02gt0  12509  dvdsval2  12535  dvdscmul  12563  dvdsmulc  12564  ndvdssub  12675  rpmulgcd  12781  cncongr1  12859  cncongr2  12860  isprm3  12874  coprimeprodsq  13014  pythagtriplem12  13032  pythagtriplem14  13034  pcmul  13058  pcdiv  13059  pcqcl  13063  pcqdiv  13064  pcdvdsb  13077  ercpbl  13629  mgmb1mgm1  13665  grpinvid1  13834  grpinvid2  13835  grpasscan1  13845  grpasscan2  13846  grpinvadd  13860  grpsubf  13861  grpsubrcan  13863  grpinvsub  13864  grpsubeq0  13868  grpsubadd0sub  13869  grppncan  13873  grpnpcan  13874  mulgnn0p1  13913  mulgaddcomlem  13925  mulginvcom  13927  mulginvinv  13928  subgsubcl  13965  subgsub  13966  eqglact  14005  quselbasg  14010  quseccl0g  14011  qussub  14017  ghmsub  14031  subcmnd  14114  rng1zrlem  14233  dvrcl  14415  unitdvcl  14416  dvrcan1  14420  dvrcan3  14421  dvreq1  14422  subrgdv  14519  lmodvsubval2  14651  lmodprop2d  14657  zndvds  14956  ntrin  15148  elnei  15176  cnrest2  15260  psmetsym  15353  psmetge0  15355  xmetge0  15389  xmetsym  15392  cnmet  15554  rpcxpsub  15933  rpdivcxp  15936  logbleb  15986  logblt  15987  lgsmodeq  16078  lgsmulsqcoprm  16079  gausslemma2dlem1a  16091  2lgsoddprmlem2  16139  upgrpredgv  16301  issubgr2  16413  uhgrissubgr  16416  egrsubgr  16418  upgrwlkvtxedg  16519  clwwlk1loop  16554  clwwlkccatlem  16555  clwwlknonex2lem2  16593  bj-peano4  16895