Theorem 3adant1 999

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 980	. 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 962

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 964

This theorem is referenced by:  3ad2ant2  1003  3ad2ant3  1004  rsp2e  2481  sbciegft  2934  reuhyp  4388  suc11g  4467  soinxp  4604  breldmg  4740  funopg  5152  funimaexglem  5201  fex2  5286  fnreseql  5523  ftpg  5597  mpoeq3ia  5829  mpofvex  6094  poxp  6122  smores3  6183  tfrlemibxssdm  6217  nndi  6375  nnmass  6376  nndir  6379  fnsnsplitdc  6394  nnaord  6398  nnaordr  6399  nnawordi  6404  nnmord  6406  ecopovtrn  6519  ecopovtrng  6522  ixpf  6607  mapxpen  6735  ltsopi  7121  addassnqg  7183  ltsonq  7199  ltmnqg  7202  distrnq0  7260  addlocpr  7337  distrlem1prl  7383  distrlem1pru  7384  distrlem4prl  7385  distrlem4pru  7386  ltpopr  7396  ltsopr  7397  addcanprg  7417  lttrsr  7563  ltsosr  7565  ltasrg  7571  recexgt0sr  7574  mulextsr1lem  7581  mulextsr1  7582  axpre-mulext  7689  adddir  7750  axltwlin  7825  axlttrn  7826  ltleletr  7839  letr  7840  mul32  7885  mul31  7886  add32  7914  subsub23  7960  addsubass  7965  subcan2  7980  subsub2  7983  nppcan2  7986  sub32  7989  nnncan  7990  nnncan2  7992  pnpcan2  7995  subdi  8140  subdir  8141  reapcotr  8353  receuap  8423  divmulap3  8430  divrecap  8441  divrecap2  8442  divsubdirap  8461  divdivap1  8476  redivclap  8484  div2negap  8488  ltmul2  8607  lemul2  8608  lemul2a  8610  lediv1  8620  gt0div  8621  ge0div  8622  ltdivmul  8627  ltdivmul2  8629  ledivmul2  8631  uzind2  9156  nn0ind  9158  fnn0ind  9160  uz3m2nn  9361  xrletr  9584  xrre2  9597  xleadd2a  9650  xleadd1  9651  xltadd2  9653  ixxdisj  9679  iooneg  9764  iccneg  9765  icoshft  9766  icoshftf1o  9767  icodisj  9768  fzen  9816  fzrev3  9860  2ffzeq  9911  fzoaddel2  9963  elfzodifsumelfzo  9971  ssfzo12bi  9995  fzoshftral  10008  adddivflid  10058  fldiv4p1lem1div2  10071  modqmulnn  10108  modqeqmodmin  10160  frec2uzf1od  10172  expdivap  10337  shftval2  10591  mulreap  10629  absdivap  10835  absdiflt  10857  absdifle  10858  abs3dif  10870  cau3  10880  ltmininf  10999  xrmaxlesup  11021  xrltmininf  11032  xrlemininf  11033  xrminltinf  11034  geoisum1c  11282  dvdsmulc  11510  dvdsmultr1  11520  dvdsmultr2  11522  dvdssub2  11524  oexpneg  11563  divalgb  11611  ndvdsadd  11617  gcdaddm  11661  modgcd  11668  dvdsgcd  11689  dvdsgcdb  11690  gcdass  11692  mulgcd  11693  absmulgcd  11694  rpmulgcd  11703  nn0seqcvgd  11711  algcvga  11721  lcmdvds  11749  lcmdvdsb  11754  lcmass  11755  coprmdvds  11762  coprmdvds2  11763  rpmul  11768  cncongr1  11773  cncongr2  11774  prmgt1  11801  qnumdenbi  11859  setsvala  11979  setsex  11980  unopn  12161  clsss  12276  opnssneib  12314  restabs  12333  upxp  12430  blpnfctr  12597  mscl  12623  xmscl  12624  xmsge0  12625  xmseq0  12626  bj-peano4  13142