Theorem 3adant1 1010

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant1

Step	Hyp	Ref	Expression
1		3simpc 991	. 2 |- ( ( th /\ ph /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( th /\ ph /\ 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:  3ad2ant2  1014  3ad2ant3  1015  rsp2e  2521  sbciegft  2985  reuhyp  4457  suc11g  4541  soinxp  4681  breldmg  4817  funopg  5232  funimaexglem  5281  fex2  5366  fnreseql  5606  ftpg  5680  mpoeq3ia  5918  funexw  6091  mpofvex  6182  poxp  6211  smores3  6272  tfrlemibxssdm  6306  nndi  6465  nnmass  6466  nndir  6469  fnsnsplitdc  6484  nnaord  6488  nnaordr  6489  nnawordi  6494  nnmord  6496  ecopovtrn  6610  ecopovtrng  6613  ixpf  6698  mapxpen  6826  ltsopi  7282  addassnqg  7344  ltsonq  7360  ltmnqg  7363  distrnq0  7421  addlocpr  7498  distrlem1prl  7544  distrlem1pru  7545  distrlem4prl  7546  distrlem4pru  7547  ltpopr  7557  ltsopr  7558  addcanprg  7578  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  mul32  8049  mul31  8050  add32  8078  subsub23  8124  addsubass  8129  subcan2  8144  subsub2  8147  nppcan2  8150  sub32  8153  nnncan  8154  nnncan2  8156  pnpcan2  8159  subdi  8304  subdir  8305  reapcotr  8517  receuap  8587  divmulap3  8594  divrecap  8605  divrecap2  8606  divsubdirap  8625  divdivap1  8640  redivclap  8648  div2negap  8652  ltmul2  8772  lemul2  8773  lemul2a  8775  lediv1  8785  gt0div  8786  ge0div  8787  ltdivmul  8792  ltdivmul2  8794  ledivmul2  8796  uzind2  9324  nn0ind  9326  fnn0ind  9328  uz3m2nn  9532  xrletr  9765  xrre2  9778  xleadd2a  9831  xleadd1  9832  xltadd2  9834  ixxdisj  9860  iooneg  9945  iccneg  9946  icoshft  9947  icoshftf1o  9948  icodisj  9949  fzen  9999  fzrev3  10043  2ffzeq  10097  fzoaddel2  10149  elfzodifsumelfzo  10157  ssfzo12bi  10181  fzoshftral  10194  adddivflid  10248  fldiv4p1lem1div2  10261  modqmulnn  10298  modqeqmodmin  10350  frec2uzf1od  10362  expdivap  10527  shftval2  10790  mulreap  10828  absdivap  11034  absdiflt  11056  absdifle  11057  abs3dif  11069  cau3  11079  ltmininf  11198  xrmaxlesup  11222  xrltmininf  11233  xrlemininf  11234  xrminltinf  11235  geoisum1c  11483  dvdsmulc  11781  dvdsmultr1  11793  dvdsmultr2  11795  dvdssub2  11797  oexpneg  11836  divalgb  11884  ndvdsadd  11890  gcdaddm  11939  modgcd  11946  dvdsgcd  11967  dvdsgcdb  11968  gcdass  11970  mulgcd  11971  absmulgcd  11972  rpmulgcd  11981  nn0seqcvgd  11995  algcvga  12005  lcmdvds  12033  lcmdvdsb  12038  lcmass  12039  coprmdvds  12046  coprmdvds2  12047  rpmul  12052  cncongr1  12057  cncongr2  12058  prmgt1  12086  qnumdenbi  12146  coprimeprodsq  12211  pythagtriplem4  12222  pythagtriplem8  12226  pythagtriplem9  12227  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem16  12233  pcpremul  12247  pcgcd  12282  setsvala  12447  setsex  12448  isgrpi  12730  unopn  12797  clsss  12912  opnssneib  12950  restabs  12969  upxp  13066  blpnfctr  13233  mscl  13259  xmscl  13260  xmsge0  13261  xmseq0  13262  rpdivcxp  13626  cxpcom  13651  rplogbreexp  13665  rplogbzexp  13666  rprelogbmulexp  13668  logbleb  13673  logblt  13674  lgsneg  13719  lgsne0  13733  lgsmodeq  13740  lgsmulsqcoprm  13741  bj-peano4  13990