Theorem 3adant2 1040

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 1019	. 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 104   /\ w3a 1002

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 1004

This theorem is referenced by:  3ad2ant1  1042  3imp3i2an  1207  eupickb  2159  vtoclegft  2876  eqeu  2974  ifnebibdc  3649  suc11g  4653  soinxp  4794  funopg  5358  fnco  5437  dff1o2  5585  fnimapr  5702  fvun1  5708  fvmptt  5734  fnreseql  5753  fvpr1g  5855  fvpr2g  5856  f1elima  5909  f1ocnvfvb  5916  ovexg  6047  oprssov  6159  poxp  6392  smoiso  6463  rdgivallem  6542  nndi  6649  nndir  6653  fnsnsplitdc  6668  nnaord  6672  nnaordr  6673  nnaword  6674  nnawordi  6678  ecopovtrn  6796  ecopovtrng  6799  xpdom3m  7013  mapxpen  7029  findcard  7070  fisseneq  7119  resfnfinfinss  7129  funrnfi  7132  netap  7463  2omotaplemap  7466  ltsopi  7530  addcanpig  7544  addassnqg  7592  distrnqg  7597  ltsonq  7608  ltmnqg  7611  prarloclemarch2  7629  nnanq0  7668  distrnq0  7669  distnq0r  7673  prltlu  7697  prarloclem5  7710  distrlem1prl  7792  distrlem1pru  7793  distrlem5prl  7796  distrlem5pru  7797  ltpopr  7805  ltsopr  7806  ltexprlemm  7810  ltexprlemfl  7819  ltexprlemfu  7821  lttrsr  7972  ltsosr  7974  ltasrg  7980  recexgt0sr  7983  mulextsr1lem  7990  mulextsr1  7991  axpre-mulext  8098  adddir  8160  axltwlin  8237  axlttrn  8238  ltleletr  8251  letr  8252  nnncan1  8405  npncan3  8407  pnpcan2  8409  subdi  8554  subdir  8555  reapcotr  8768  divmulap  8845  div23ap  8861  div13ap  8863  muldivdirap  8877  divsubdirap  8878  divcanap7  8891  ltmul2  9026  lemul2  9027  lemul2a  9029  lediv1  9039  ltmuldiv2  9045  lemuldiv2  9052  squeeze0  9074  nndivtr  9175  bndndx  9391  nn0n0n1ge2  9540  fnn0ind  9586  addlelt  9993  xrletr  10033  xrltne  10038  xleadd2a  10099  xleadd1  10100  xltadd2  10102  iooneg  10213  iccneg  10214  icoshft  10215  icoshftf1o  10216  zltaddlt1le  10232  fztri3or  10264  fzdcel  10265  fzen  10268  uzsubsubfz  10272  fzrevral2  10331  fzshftral  10333  fz0fzdiffz0  10355  elfzmlbp  10357  elfzo  10374  nelfzo  10377  fzoaddel2  10425  fzosubel2  10430  elfzom1p1elfzo  10449  ssfzo12bi  10460  subfzo0  10478  flltdivnn0lt  10554  modqmulnn  10594  modfzo0difsn  10647  expdivap  10842  expubnd  10848  mulbinom2  10908  bernneq2  10913  ccatval1  11164  ccatval3  11166  ccatfv0  11170  ccatval1lsw  11171  ccatws1lenp1bg  11202  pfxsuffeqwrdeq  11269  pfxsuff1eqwrdeq  11270  swrdswrd  11276  pfxpfx  11279  wrd2ind  11294  swrdccatin1  11296  pfxccatin12lem1  11299  swrdccatin2  11300  pfxccatin12lem3  11303  swrdccat  11306  pfxccatpfx1  11307  pfxccatpfx2  11308  swrdccat3blem  11310  shftuz  11368  shftval2  11377  abs3dif  11656  xrmaxlesup  11810  xrltmininf  11821  xrlemininf  11822  sin02gt0  12315  dvdsval2  12341  dvdscmul  12369  dvdsmulc  12370  ndvdssub  12481  rpmulgcd  12587  cncongr1  12665  cncongr2  12666  isprm3  12680  coprimeprodsq  12820  pythagtriplem12  12838  pythagtriplem14  12840  pcmul  12864  pcdiv  12865  pcqcl  12869  pcqdiv  12870  pcdvdsb  12883  ercpbl  13404  mgmb1mgm1  13441  grpinvid1  13625  grpinvid2  13626  grpasscan1  13636  grpasscan2  13637  grpinvadd  13651  grpsubf  13652  grpsubrcan  13654  grpinvsub  13655  grpsubeq0  13659  grpsubadd0sub  13660  grppncan  13664  grpnpcan  13665  mulgnn0p1  13710  mulgaddcomlem  13722  mulginvcom  13724  mulginvinv  13725  subgsubcl  13762  subgsub  13763  eqglact  13802  quselbasg  13807  quseccl0g  13808  qussub  13814  ghmsub  13828  subcmnd  13910  srg1zr  13990  dvrcl  14139  unitdvcl  14140  dvrcan1  14144  dvrcan3  14145  dvreq1  14146  subrgdv  14242  lmodvsubval2  14346  lmodprop2d  14352  zndvds  14653  ntrin  14838  elnei  14866  cnrest2  14950  psmetsym  15043  psmetge0  15045  xmetge0  15079  xmetsym  15082  cnmet  15244  rpcxpsub  15622  rpdivcxp  15625  logbleb  15675  logblt  15676  lgsmodeq  15764  lgsmulsqcoprm  15765  gausslemma2dlem1a  15777  2lgsoddprmlem2  15825  upgrpredgv  15985  upgrwlkvtxedg  16161  clwwlk1loop  16194  clwwlkccatlem  16195  clwwlknonex2lem2  16233  bj-peano4  16486