Theorem 3adant1 1018

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 999	. 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 104   /\ w3a 981

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 983

This theorem is referenced by:  3ad2ant2  1022  3ad2ant3  1023  rsp2e  2557  sbciegft  3029  reuhyp  4519  suc11g  4605  soinxp  4745  breldmg  4884  funopg  5305  funimaexglem  5357  fex2  5444  fnreseql  5690  ftpg  5768  mpoeq3ia  6010  funexw  6197  mpofvex  6291  poxp  6318  smores3  6379  tfrlemibxssdm  6413  nndi  6572  nnmass  6573  nndir  6576  fnsnsplitdc  6591  nnaord  6595  nnaordr  6596  nnawordi  6601  nnmord  6603  ecopovtrn  6719  ecopovtrng  6722  ixpf  6807  f1oen4g  6843  f1dom4g  6844  mapxpen  6945  netap  7366  2omotaplemap  7369  ltsopi  7433  addassnqg  7495  ltsonq  7511  ltmnqg  7514  distrnq0  7572  addlocpr  7649  distrlem1prl  7695  distrlem1pru  7696  distrlem4prl  7697  distrlem4pru  7698  ltpopr  7708  ltsopr  7709  addcanprg  7729  lttrsr  7875  ltsosr  7877  ltasrg  7883  recexgt0sr  7886  mulextsr1lem  7893  mulextsr1  7894  axpre-mulext  8001  adddir  8063  axltwlin  8140  axlttrn  8141  ltleletr  8154  letr  8155  mul32  8202  mul31  8203  add32  8231  subsub23  8277  addsubass  8282  subcan2  8297  subsub2  8300  nppcan2  8303  sub32  8306  nnncan  8307  nnncan2  8309  pnpcan2  8312  subdi  8457  subdir  8458  reapcotr  8671  receuap  8742  divmulap3  8750  divrecap  8761  divrecap2  8762  divsubdirap  8781  divdivap1  8796  redivclap  8804  div2negap  8808  ltmul2  8929  lemul2  8930  lemul2a  8932  lediv1  8942  gt0div  8943  ge0div  8944  ltdivmul  8949  ltdivmul2  8951  ledivmul2  8953  uzind2  9485  nn0ind  9487  fnn0ind  9489  uz3m2nn  9694  xrletr  9930  xrre2  9943  xleadd2a  9996  xleadd1  9997  xltadd2  9999  ixxdisj  10025  iooneg  10110  iccneg  10111  icoshft  10112  icoshftf1o  10113  icodisj  10114  fzen  10165  fzrev3  10209  2ffzeq  10263  fzoaddel2  10319  elfzodifsumelfzo  10330  ssfzo12bi  10354  fzoshftral  10367  adddivflid  10435  fldiv4p1lem1div2  10448  modqmulnn  10487  modqeqmodmin  10539  frec2uzf1od  10551  expdivap  10735  ccatval1  11053  ccatass  11064  fzowrddc  11100  swrdval  11101  swrdnd  11112  swrd0g  11113  swrdfv2  11116  shftval2  11137  mulreap  11175  absdivap  11381  absdiflt  11403  absdifle  11404  abs3dif  11416  cau3  11426  ltmininf  11546  xrmaxlesup  11570  xrltmininf  11581  xrlemininf  11582  xrminltinf  11583  geoisum1c  11831  dvdsmulc  12130  dvdsmultr1  12142  dvdsmultr2  12144  dvdssub2  12146  oexpneg  12188  divalgb  12236  ndvdsadd  12242  gcdaddm  12305  modgcd  12312  dvdsgcd  12333  dvdsgcdb  12334  gcdass  12336  mulgcd  12337  absmulgcd  12338  rpmulgcd  12347  nn0seqcvgd  12363  algcvga  12373  lcmdvds  12401  lcmdvdsb  12406  lcmass  12407  coprmdvds  12414  coprmdvds2  12415  rpmul  12420  cncongr1  12425  cncongr2  12426  prmgt1  12454  qnumdenbi  12514  coprimeprodsq  12580  pythagtriplem4  12591  pythagtriplem8  12595  pythagtriplem9  12596  pythagtriplem12  12598  pythagtriplem14  12600  pythagtriplem16  12602  pcpremul  12616  pcgcd  12652  setsvala  12863  setsex  12864  ressval2  12898  isgrpi  13356  grpsubrcan  13413  grpinvsub  13414  grpsubeq0  13418  grpsubadd0sub  13419  grpnpcan  13424  qussub  13573  ghmsub  13587  opprmulg  13833  rrgeq0  14027  lmodvsubval2  14104  rmodislmodlem  14112  rmodislmod  14113  lssintclm  14146  lssincl  14147  rnglidlmmgm  14258  cncrng  14331  unopn  14477  clsss  14590  opnssneib  14628  restabs  14647  upxp  14744  blpnfctr  14911  mscl  14937  xmscl  14938  xmsge0  14939  xmseq0  14940  mpomulcn  15038  rpdivcxp  15383  cxpcom  15410  rplogbreexp  15425  rplogbzexp  15426  rprelogbmulexp  15428  logbleb  15433  logblt  15434  lgsneg  15501  lgsne0  15515  lgsmodeq  15522  lgsmulsqcoprm  15523  gausslemma2dlem1a  15535  funvtxdm2domval  15626  funiedgdm2domval  15627  bj-peano4  15891