Theorem 3adant2 1042

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 1021	. 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 1004

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 1006

This theorem is referenced by:  3ad2ant1  1044  3imp3i2an  1209  eupickb  2161  vtoclegft  2878  eqeu  2976  ifnebibdc  3651  suc11g  4655  soinxp  4796  funopg  5360  fnco  5440  dff1o2  5588  fnimapr  5706  fvun1  5712  fvmptt  5738  fnreseql  5757  fvpr1g  5860  fvpr2g  5861  f1elima  5914  f1ocnvfvb  5921  ovexg  6052  oprssov  6164  poxp  6397  smoiso  6468  rdgivallem  6547  nndi  6654  nndir  6658  fnsnsplitdc  6673  nnaord  6677  nnaordr  6678  nnaword  6679  nnawordi  6683  ecopovtrn  6801  ecopovtrng  6804  xpdom3m  7018  mapxpen  7034  findcard  7077  fisseneq  7127  resfnfinfinss  7138  funrnfi  7141  netap  7473  2omotaplemap  7476  ltsopi  7540  addcanpig  7554  addassnqg  7602  distrnqg  7607  ltsonq  7618  ltmnqg  7621  prarloclemarch2  7639  nnanq0  7678  distrnq0  7679  distnq0r  7683  prltlu  7707  prarloclem5  7720  distrlem1prl  7802  distrlem1pru  7803  distrlem5prl  7806  distrlem5pru  7807  ltpopr  7815  ltsopr  7816  ltexprlemm  7820  ltexprlemfl  7829  ltexprlemfu  7831  lttrsr  7982  ltsosr  7984  ltasrg  7990  recexgt0sr  7993  mulextsr1lem  8000  mulextsr1  8001  axpre-mulext  8108  adddir  8170  axltwlin  8247  axlttrn  8248  ltleletr  8261  letr  8262  nnncan1  8415  npncan3  8417  pnpcan2  8419  subdi  8564  subdir  8565  reapcotr  8778  divmulap  8855  div23ap  8871  div13ap  8873  muldivdirap  8887  divsubdirap  8888  divcanap7  8901  ltmul2  9036  lemul2  9037  lemul2a  9039  lediv1  9049  ltmuldiv2  9055  lemuldiv2  9062  squeeze0  9084  nndivtr  9185  bndndx  9401  nn0n0n1ge2  9550  fnn0ind  9596  addlelt  10003  xrletr  10043  xrltne  10048  xleadd2a  10109  xleadd1  10110  xltadd2  10112  iooneg  10223  iccneg  10224  icoshft  10225  icoshftf1o  10226  zltaddlt1le  10242  fztri3or  10274  fzdcel  10275  fzen  10278  uzsubsubfz  10282  fzrevral2  10341  fzshftral  10343  fz0fzdiffz0  10365  elfzmlbp  10367  elfzo  10384  nelfzo  10387  fzoaddel2  10436  fzosubel2  10441  elfzom1p1elfzo  10460  ssfzo12bi  10471  subfzo0  10489  flltdivnn0lt  10565  modqmulnn  10605  modfzo0difsn  10658  expdivap  10853  expubnd  10859  mulbinom2  10919  bernneq2  10924  ccatval1  11178  ccatval3  11180  ccatfv0  11184  ccatval1lsw  11185  ccatws1lenp1bg  11216  pfxsuffeqwrdeq  11283  pfxsuff1eqwrdeq  11284  swrdswrd  11290  pfxpfx  11293  wrd2ind  11308  swrdccatin1  11310  pfxccatin12lem1  11313  swrdccatin2  11314  pfxccatin12lem3  11317  swrdccat  11320  pfxccatpfx1  11321  pfxccatpfx2  11322  swrdccat3blem  11324  shftuz  11395  shftval2  11404  abs3dif  11683  xrmaxlesup  11837  xrltmininf  11848  xrlemininf  11849  sin02gt0  12343  dvdsval2  12369  dvdscmul  12397  dvdsmulc  12398  ndvdssub  12509  rpmulgcd  12615  cncongr1  12693  cncongr2  12694  isprm3  12708  coprimeprodsq  12848  pythagtriplem12  12866  pythagtriplem14  12868  pcmul  12892  pcdiv  12893  pcqcl  12897  pcqdiv  12898  pcdvdsb  12911  ercpbl  13432  mgmb1mgm1  13469  grpinvid1  13653  grpinvid2  13654  grpasscan1  13664  grpasscan2  13665  grpinvadd  13679  grpsubf  13680  grpsubrcan  13682  grpinvsub  13683  grpsubeq0  13687  grpsubadd0sub  13688  grppncan  13692  grpnpcan  13693  mulgnn0p1  13738  mulgaddcomlem  13750  mulginvcom  13752  mulginvinv  13753  subgsubcl  13790  subgsub  13791  eqglact  13830  quselbasg  13835  quseccl0g  13836  qussub  13842  ghmsub  13856  subcmnd  13938  srg1zr  14019  dvrcl  14168  unitdvcl  14169  dvrcan1  14173  dvrcan3  14174  dvreq1  14175  subrgdv  14271  lmodvsubval2  14375  lmodprop2d  14381  zndvds  14682  ntrin  14867  elnei  14895  cnrest2  14979  psmetsym  15072  psmetge0  15074  xmetge0  15108  xmetsym  15111  cnmet  15273  rpcxpsub  15651  rpdivcxp  15654  logbleb  15704  logblt  15705  lgsmodeq  15793  lgsmulsqcoprm  15794  gausslemma2dlem1a  15806  2lgsoddprmlem2  15854  upgrpredgv  16016  issubgr2  16128  uhgrissubgr  16131  egrsubgr  16133  upgrwlkvtxedg  16234  clwwlk1loop  16269  clwwlkccatlem  16270  clwwlknonex2lem2  16308  bj-peano4  16601