Theorem 3adant2 1047

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 1026	. 2 |- ( ( ph /\ th /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( ph /\ th /\ 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:  3ad2ant1  1049  3imp3i2an  1214  eupickb  2168  vtoclegft  2897  eqeu  2996  ifnebibdc  3686  suc11g  4704  soinxp  4845  funopg  5411  fnco  5491  dff1o2  5644  fnimapr  5763  fvun1  5769  fvmptt  5797  fnreseql  5819  fvpr1g  5921  fvpr2g  5922  f1elima  5979  f1ocnvfvb  5986  ovexg  6119  oprssov  6231  poxp  6468  smoiso  6573  rdgivallem  6652  nndi  6759  nndir  6763  fnsnsplitdc  6778  nnaord  6782  nnaordr  6783  nnaword  6784  nnawordi  6788  ecopovtrn  6906  ecopovtrng  6909  mapsnd  6970  xpdom3m  7132  mapxpen  7148  findcard  7192  fisseneq  7242  resfnfinfinss  7253  funrnfi  7256  netap  7621  2omotaplemap  7624  ltsopi  7688  addcanpig  7702  addassnqg  7750  distrnqg  7755  ltsonq  7766  ltmnqg  7769  prarloclemarch2  7787  nnanq0  7826  distrnq0  7827  distnq0r  7831  prltlu  7855  prarloclem5  7868  distrlem1prl  7950  distrlem1pru  7951  distrlem5prl  7954  distrlem5pru  7955  ltpopr  7963  ltsopr  7964  ltexprlemm  7968  ltexprlemfl  7977  ltexprlemfu  7979  lttrsr  8130  ltsosr  8132  ltasrg  8138  recexgt0sr  8141  mulextsr1lem  8148  mulextsr1  8149  axpre-mulext  8256  adddir  8318  axltwlin  8394  axlttrn  8395  ltleletr  8408  letr  8409  nnncan1  8564  npncan3  8566  pnpcan2  8568  subdi  8714  subdir  8715  reapcotr  8929  divmulap  9008  div23ap  9024  div13ap  9026  muldivdirap  9040  divsubdirap  9041  divcanap7  9054  ltmul2  9189  lemul2  9190  lemul2a  9192  lediv1  9202  ltmuldiv2  9208  lemuldiv2  9215  squeeze0  9237  nndivtr  9349  bndndx  9567  nn0n0n1ge2  9720  fnn0ind  9767  addlelt  10180  xrletr  10221  xrltne  10226  xleadd2a  10287  xleadd1  10288  xltadd2  10290  iooneg  10401  iccneg  10402  icoshft  10403  icoshftf1o  10404  zltaddlt1le  10421  fztri3or  10454  fzdcel  10455  fzen  10458  uzsubsubfz  10463  fzrevral2  10524  fzshftral  10526  fz0fzdiffz0  10548  elfzmlbp  10550  elfzo  10567  nelfzo  10570  fzoaddel2  10619  fzosubel2  10624  elfzom1p1elfzo  10643  ssfzo12bi  10654  subfzo0  10672  flltdivnn0lt  10754  modqmulnn  10794  modfzo0difsn  10847  expdivap  11042  expubnd  11048  mulbinom2  11108  bernneq2  11114  ccatval1  11381  ccatval3  11383  ccatfv0  11387  ccatval1lsw  11388  ccatws1lenp1bg  11419  pfxsuffeqwrdeq  11486  pfxsuff1eqwrdeq  11487  swrdswrd  11493  pfxpfx  11496  wrd2ind  11511  swrdccatin1  11513  pfxccatin12lem1  11516  swrdccatin2  11517  pfxccatin12lem3  11520  swrdccat  11523  pfxccatpfx1  11524  pfxccatpfx2  11525  swrdccat3blem  11527  shftuz  11598  shftval2  11607  abs3dif  11888  xrmaxlesup  12044  xrltmininf  12055  xrlemininf  12056  sin02gt0  12550  dvdsval2  12576  dvdscmul  12604  dvdsmulc  12605  ndvdssub  12716  rpmulgcd  12822  cncongr1  12900  cncongr2  12901  isprm3  12915  coprimeprodsq  13059  pythagtriplem12  13077  pythagtriplem14  13079  pcmul  13103  pcdiv  13104  pcqcl  13108  pcqdiv  13109  pcdvdsb  13122  ercpbl  13705  mgmb1mgm1  13741  grpinvid1  13910  grpinvid2  13911  grpasscan1  13921  grpasscan2  13922  grpinvadd  13936  grpsubf  13937  grpsubrcan  13939  grpinvsub  13940  grpsubeq0  13944  grpsubadd0sub  13945  grppncan  13949  grpnpcan  13950  mulgnn0p1  13989  mulgaddcomlem  14001  mulginvcom  14003  mulginvinv  14004  subgsubcl  14041  subgsub  14042  eqglact  14081  quselbasg  14086  quseccl0g  14087  qussub  14093  ghmsub  14107  subcmnd  14221  rng1zrlem  14342  dvrcl  14526  unitdvcl  14527  dvrcan1  14531  dvrcan3  14532  dvreq1  14533  subrgdv  14630  lmodvsubval2  14763  lmodprop2d  14769  zndvds  15068  ascldimul  15115  ntrin  15316  elnei  15344  cnrest2  15428  psmetsym  15521  psmetge0  15523  xmetge0  15557  xmetsym  15560  cnmet  15722  rpcxpsub  16105  rpdivcxp  16108  logbleb  16158  logblt  16159  lgsmodeq  16330  lgsmulsqcoprm  16331  gausslemma2dlem1a  16343  2lgsoddprmlem2  16391  upgrpredgv  16553  issubgr2  16665  uhgrissubgr  16668  egrsubgr  16670  upgrwlkvtxedg  16771  clwwlk1loop  16806  clwwlkccatlem  16807  clwwlknonex2lem2  16845  bj-peano4  17147