Theorem 3adant1 1046

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 1027	. 2 |- ( ( th /\ ph /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( th /\ ph /\ ps ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3ad2ant2  1050  3ad2ant3  1051  rsp2e  2601  sbciegft  3082  reuhyp  4620  suc11g  4706  soinxp  4847  breldmg  4989  funopg  5414  funimaexglem  5467  fex2  5559  fnreseql  5822  ftpg  5902  mpoeq3ia  6156  funexw  6345  mpofvex  6445  poxp  6472  suppval1  6483  smores3  6568  tfrlemibxssdm  6602  nndi  6763  nnmass  6764  nndir  6767  fnsnsplitdc  6782  nnaord  6786  nnaordr  6787  nnawordi  6792  nnmord  6794  ecopovtrn  6910  ecopovtrng  6913  ixpf  7006  f1oen4g  7042  f1dom4g  7043  mapxpen  7152  funisfsupp  7296  netap  7626  2omotaplemap  7629  ltsopi  7693  addassnqg  7755  ltsonq  7771  ltmnqg  7774  distrnq0  7832  addlocpr  7909  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  ltpopr  7968  ltsopr  7969  addcanprg  7989  lttrsr  8135  ltsosr  8137  ltasrg  8143  recexgt0sr  8146  mulextsr1lem  8153  mulextsr1  8154  axpre-mulext  8261  adddir  8323  axltwlin  8399  axlttrn  8400  ltleletr  8413  letr  8414  mul32  8463  mul31  8464  add32  8492  subsub23  8538  addsubass  8543  subcan2  8558  subsub2  8561  nppcan2  8564  sub32  8567  nnncan  8568  nnncan2  8570  pnpcan2  8573  subdi  8719  subdir  8720  reapcotr  8934  receuap  9007  divmulap3  9015  divrecap  9026  divrecap2  9027  divsubdirap  9046  divdivap1  9061  redivclap  9069  div2negap  9073  ltmul2  9194  lemul2  9195  lemul2a  9197  lediv1  9207  gt0div  9208  ge0div  9209  ltdivmul  9214  ltdivmul2  9216  ledivmul2  9218  uzind2  9769  nn0ind  9771  fnn0ind  9773  uz3m2nn  9989  xrletr  10227  xrre2  10240  xleadd2a  10293  xleadd1  10294  xltadd2  10296  ixxdisj  10322  iooneg  10407  iccneg  10408  icoshft  10409  icoshftf1o  10410  icodisj  10411  fzen  10464  fzrev3  10511  2ffzeq  10565  fzoaddel2  10625  elfzodifsumelfzo  10636  ssfzo12bi  10660  fzoshftral  10674  adddivflid  10748  fldiv4p1lem1div2  10761  modqmulnn  10800  modqeqmodmin  10852  frec2uzf1od  10864  expdivap  11048  ccatval1  11387  ccatass  11398  fzowrddc  11441  swrdval  11442  swrdnd  11453  swrd0g  11454  swrdfv2  11457  pfxsuff1eqwrdeq  11493  swrdswrdlem  11498  pfxccatin12lem2a  11521  pfxccatin12lem1  11522  shftval2  11613  mulreap  11651  absdivap  11858  absdiflt  11881  absdifle  11882  abs3dif  11894  cau3  11904  ltmininf  12025  xrmaxlesup  12050  xrltmininf  12061  xrlemininf  12062  xrminltinf  12063  geoisum1c  12312  dvdsmulc  12611  dvdsmultr1  12623  dvdsmultr2  12625  dvdssub2  12627  oexpneg  12669  divalgb  12717  ndvdsadd  12723  gcdaddm  12786  modgcd  12793  dvdsgcd  12814  dvdsgcdb  12815  gcdass  12817  mulgcd  12818  absmulgcd  12819  rpmulgcd  12828  nn0seqcvgd  12844  algcvga  12854  lcmdvds  12882  lcmdvdsb  12887  lcmass  12888  coprmdvds  12895  coprmdvds2  12896  rpmul  12901  cncongr1  12906  cncongr2  12907  prmgt1  12936  qnumdenbi  12997  coprimeprodsq  13065  pythagtriplem4  13076  pythagtriplem8  13080  pythagtriplem9  13081  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem16  13087  pcpremul  13101  pcgcd  13137  setsvala  13441  setsex  13442  ressval2  13479  isgrpi  13888  grpsubrcan  13945  grpinvsub  13946  grpsubeq0  13950  grpsubadd0sub  13951  grpnpcan  13956  qussub  14099  ghmsub  14113  opprmulg  14485  rrgeq0  14682  lmodvsubval2  14788  rmodislmodlem  14796  rmodislmod  14797  lssintclm  14830  lssincl  14831  rnglidlmmgm  14942  cncrng  15015  unopn  15231  clsss  15344  opnssneib  15382  restabs  15401  upxp  15498  blpnfctr  15665  mscl  15691  xmscl  15692  xmsge0  15693  xmseq0  15694  mpomulcn  15792  rpdivcxp  16144  cxpcom  16173  rplogbreexp  16189  rplogbzexp  16190  rprelogbmulexp  16192  logbleb  16197  logblt  16198  lgsneg  16348  lgsne0  16362  lgsmodeq  16369  lgsmulsqcoprm  16370  gausslemma2dlem1a  16382  funvtxdm2domval  16475  funiedgdm2domval  16476  iedgedgg  16507  iswlk  16769  uspgr2wlkeq  16811  uspgr2wlkeq2  16812  uspgr2wlkeqi  16813  istrl  16831  clwwlkgt0  16842  iseupth  16893  bj-peano4  17186