Theorem 3adant2 1011

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 990	. 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 103   /\ w3a 973

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

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  3ad2ant1  1013  3imp3i2an  1178  eupickb  2100  vtoclegft  2802  eqeu  2900  suc11g  4541  soinxp  4681  funopg  5232  fnco  5306  dff1o2  5447  fnimapr  5556  fvun1  5562  fvmptt  5587  fnreseql  5606  fvpr1g  5702  fvpr2g  5703  f1elima  5752  f1ocnvfvb  5759  ovexg  5887  oprssov  5994  poxp  6211  smoiso  6281  rdgivallem  6360  nndi  6465  nndir  6469  fnsnsplitdc  6484  nnaord  6488  nnaordr  6489  nnaword  6490  nnawordi  6494  ecopovtrn  6610  ecopovtrng  6613  xpdom3m  6812  mapxpen  6826  findcard  6866  fisseneq  6909  resfnfinfinss  6917  funrnfi  6919  ltsopi  7282  addcanpig  7296  addassnqg  7344  distrnqg  7349  ltsonq  7360  ltmnqg  7363  prarloclemarch2  7381  nnanq0  7420  distrnq0  7421  distnq0r  7425  prltlu  7449  prarloclem5  7462  distrlem1prl  7544  distrlem1pru  7545  distrlem5prl  7548  distrlem5pru  7549  ltpopr  7557  ltsopr  7558  ltexprlemm  7562  ltexprlemfl  7571  ltexprlemfu  7573  lttrsr  7724  ltsosr  7726  ltasrg  7732  recexgt0sr  7735  mulextsr1lem  7742  mulextsr1  7743  axpre-mulext  7850  adddir  7911  axltwlin  7987  axlttrn  7988  ltleletr  8001  letr  8002  nnncan1  8155  npncan3  8157  pnpcan2  8159  subdi  8304  subdir  8305  reapcotr  8517  divmulap  8592  div23ap  8608  div13ap  8610  muldivdirap  8624  divsubdirap  8625  divcanap7  8638  ltmul2  8772  lemul2  8773  lemul2a  8775  lediv1  8785  ltmuldiv2  8791  lemuldiv2  8798  squeeze0  8820  nndivtr  8920  bndndx  9134  nn0n0n1ge2  9282  fnn0ind  9328  addlelt  9725  xrletr  9765  xrltne  9770  xleadd2a  9831  xleadd1  9832  xltadd2  9834  iooneg  9945  iccneg  9946  icoshft  9947  icoshftf1o  9948  zltaddlt1le  9964  fztri3or  9995  fzdcel  9996  fzen  9999  uzsubsubfz  10003  fzrevral2  10062  fzshftral  10064  fz0fzdiffz0  10086  elfzmlbp  10088  elfzo  10105  fzoaddel2  10149  fzosubel2  10151  elfzom1p1elfzo  10170  ssfzo12bi  10181  subfzo0  10198  flltdivnn0lt  10260  modqmulnn  10298  modfzo0difsn  10351  expdivap  10527  expubnd  10533  mulbinom2  10592  bernneq2  10597  shftuz  10781  shftval2  10790  abs3dif  11069  xrmaxlesup  11222  xrltmininf  11233  xrlemininf  11234  sin02gt0  11726  dvdsval2  11752  dvdscmul  11780  dvdsmulc  11781  ndvdssub  11889  rpmulgcd  11981  cncongr1  12057  cncongr2  12058  isprm3  12072  coprimeprodsq  12211  pythagtriplem12  12229  pythagtriplem14  12231  pcmul  12255  pcdiv  12256  pcqcl  12260  pcqdiv  12261  pcdvdsb  12273  mgmb1mgm1  12622  grpinvid1  12754  grpinvid2  12755  grpasscan1  12762  grpasscan2  12763  ntrin  12918  elnei  12946  cnrest2  13030  psmetsym  13123  psmetge0  13125  xmetge0  13159  xmetsym  13162  cnmet  13324  rpcxpsub  13623  rpdivcxp  13626  logbleb  13673  logblt  13674  lgsmodeq  13740  lgsmulsqcoprm  13741  bj-peano4  13990