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  5859  fvpr2g  5860  f1elima  5913  f1ocnvfvb  5920  ovexg  6051  oprssov  6163  poxp  6396  smoiso  6467  rdgivallem  6546  nndi  6653  nndir  6657  fnsnsplitdc  6672  nnaord  6676  nnaordr  6677  nnaword  6678  nnawordi  6682  ecopovtrn  6800  ecopovtrng  6803  xpdom3m  7017  mapxpen  7033  findcard  7076  fisseneq  7126  resfnfinfinss  7137  funrnfi  7140  netap  7472  2omotaplemap  7475  ltsopi  7539  addcanpig  7553  addassnqg  7601  distrnqg  7606  ltsonq  7617  ltmnqg  7620  prarloclemarch2  7638  nnanq0  7677  distrnq0  7678  distnq0r  7682  prltlu  7706  prarloclem5  7719  distrlem1prl  7801  distrlem1pru  7802  distrlem5prl  7805  distrlem5pru  7806  ltpopr  7814  ltsopr  7815  ltexprlemm  7819  ltexprlemfl  7828  ltexprlemfu  7830  lttrsr  7981  ltsosr  7983  ltasrg  7989  recexgt0sr  7992  mulextsr1lem  7999  mulextsr1  8000  axpre-mulext  8107  adddir  8169  axltwlin  8246  axlttrn  8247  ltleletr  8260  letr  8261  nnncan1  8414  npncan3  8416  pnpcan2  8418  subdi  8563  subdir  8564  reapcotr  8777  divmulap  8854  div23ap  8870  div13ap  8872  muldivdirap  8886  divsubdirap  8887  divcanap7  8900  ltmul2  9035  lemul2  9036  lemul2a  9038  lediv1  9048  ltmuldiv2  9054  lemuldiv2  9061  squeeze0  9083  nndivtr  9184  bndndx  9400  nn0n0n1ge2  9549  fnn0ind  9595  addlelt  10002  xrletr  10042  xrltne  10047  xleadd2a  10108  xleadd1  10109  xltadd2  10111  iooneg  10222  iccneg  10223  icoshft  10224  icoshftf1o  10225  zltaddlt1le  10241  fztri3or  10273  fzdcel  10274  fzen  10277  uzsubsubfz  10281  fzrevral2  10340  fzshftral  10342  fz0fzdiffz0  10364  elfzmlbp  10366  elfzo  10383  nelfzo  10386  fzoaddel2  10434  fzosubel2  10439  elfzom1p1elfzo  10458  ssfzo12bi  10469  subfzo0  10487  flltdivnn0lt  10563  modqmulnn  10603  modfzo0difsn  10656  expdivap  10851  expubnd  10857  mulbinom2  10917  bernneq2  10922  ccatval1  11173  ccatval3  11175  ccatfv0  11179  ccatval1lsw  11180  ccatws1lenp1bg  11211  pfxsuffeqwrdeq  11278  pfxsuff1eqwrdeq  11279  swrdswrd  11285  pfxpfx  11288  wrd2ind  11303  swrdccatin1  11305  pfxccatin12lem1  11308  swrdccatin2  11309  pfxccatin12lem3  11312  swrdccat  11315  pfxccatpfx1  11316  pfxccatpfx2  11317  swrdccat3blem  11319  shftuz  11377  shftval2  11386  abs3dif  11665  xrmaxlesup  11819  xrltmininf  11830  xrlemininf  11831  sin02gt0  12324  dvdsval2  12350  dvdscmul  12378  dvdsmulc  12379  ndvdssub  12490  rpmulgcd  12596  cncongr1  12674  cncongr2  12675  isprm3  12689  coprimeprodsq  12829  pythagtriplem12  12847  pythagtriplem14  12849  pcmul  12873  pcdiv  12874  pcqcl  12878  pcqdiv  12879  pcdvdsb  12892  ercpbl  13413  mgmb1mgm1  13450  grpinvid1  13634  grpinvid2  13635  grpasscan1  13645  grpasscan2  13646  grpinvadd  13660  grpsubf  13661  grpsubrcan  13663  grpinvsub  13664  grpsubeq0  13668  grpsubadd0sub  13669  grppncan  13673  grpnpcan  13674  mulgnn0p1  13719  mulgaddcomlem  13731  mulginvcom  13733  mulginvinv  13734  subgsubcl  13771  subgsub  13772  eqglact  13811  quselbasg  13816  quseccl0g  13817  qussub  13823  ghmsub  13837  subcmnd  13919  srg1zr  13999  dvrcl  14148  unitdvcl  14149  dvrcan1  14153  dvrcan3  14154  dvreq1  14155  subrgdv  14251  lmodvsubval2  14355  lmodprop2d  14361  zndvds  14662  ntrin  14847  elnei  14875  cnrest2  14959  psmetsym  15052  psmetge0  15054  xmetge0  15088  xmetsym  15091  cnmet  15253  rpcxpsub  15631  rpdivcxp  15634  logbleb  15684  logblt  15685  lgsmodeq  15773  lgsmulsqcoprm  15774  gausslemma2dlem1a  15786  2lgsoddprmlem2  15834  upgrpredgv  15996  issubgr2  16108  uhgrissubgr  16111  egrsubgr  16113  upgrwlkvtxedg  16214  clwwlk1loop  16249  clwwlkccatlem  16250  clwwlknonex2lem2  16288  bj-peano4  16550