Theorem 3adant2 810

Description: Deduction adding a conjunct to antecedent.

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

Syntax hints:   -> wi 3   /\ wa 230   /\ w3a 787

This theorem is referenced by:  3ad2ant1 812  3adantl2 816  eupickb 1478  ordunel 3141  funopg 3604  fnco 3652  f1ocnvfvb 3939  oprssoprval 4092  curry1val 4158  oaord 4239  omcan 4258  omwordri 4261  odi 4268  oecan 4274  oewordri 4277  oeordsuc 4279  nnaordr 4294  ecopoprtrn 4372  eceqopreq 4374  fodomr 4546  ltsopi 5081  ltsopq 5140  ltsopr 5201  ltsosr 5268  ltasr 5274  adddir 5384  addcan2 5418  subcan2 5467  subcan 5477  subdi 5492  subdir 5493  nnncan1 5532  pnpcan2 5544  pnncan 5545  axlttrn 5569  letr 5590  xrletr 5629  ltadd2 5689  leadd2 5691  lesub1 5725  lesub2 5726  ltsub1 5727  ltsub2 5728  mulcan2 5757  mulcan2OLD 5758  div13 5806  divsubdir 5832  ltmul2 5889  lemul1 5890  lemul2 5891  lemul2a 5897  lemul2aOLD 5898  lediv1 5909  ltmuldiv2 5923  lt2mul2div 5931  lemuldiv 5934  lemuldiv2 5936  ltdiv2 5947  lediv2 5951  nndivtr 6021  bndndx 6155  supxrbnd 6173  uzwo3lem1 6301  qsqueeze 6333  modcyc 6376  modcycOLD 6377  iooss1 6398  iooss2 6399  eliooord 6413  iooneg 6432  iccneg 6433  icoshf 6434  ioojoin 6442  elfz2nn0 6521  fzrev2i 6539  fzrevral2 6546  fzshftral 6548  shftval2 6606  expsub 6687  expwordi 6692  expword2i 6694  expubnd 6697  bernneq2 6742  abs3dif 6989  seq1ubi 7002  fsumshf 7121  fsumshftm 7122  caucvglem2 7248  isummulc1iALT 7303  cvgratlem5 7344  cncffvrn 7363  sin02gt0 7570  infxpidmlem4 7647  infxp 7664  istps3 7699  iincld 7764  neiint 7804  elnei 7810  islp2 7832  cnco 7853  cncnp 7863  cnconst 7865  metsym 7901  metge0 7904  metxplem3 7913  metxplem4 7918  blin 7937  ssbl 7940  metcnpf 7968  metcnp 7972  metcnpi3 7977  metcnpi4 7978  metcnss 7983  metcnss2 7984  cnmet 7989  dscmet 8003  lmuni 8036  metcnp4 8055  iscms2lem4 8077  isgrp 8126  grpinvid1 8156  grpinvid2 8157  grpasscan1 8161  grpinvop 8164  grpdivinv 8167  grpinvdiv 8168  grpdivf 8169  grppncan 8174  grpnpcan 8175  grppnpcan2 8176  resgrprn 8179  ablnncan 8196  vcnegsubdi2 8278  vcsub4 8279  nvmval 8347  nvmul0or 8356  nvsubadd 8359  nvpncan2 8360  nvaddsub4 8365  nvnncan 8367  nvmeq0 8368  nvdif 8377  nvpi 8378  nvmtri 8383  nvabs 8385  imsmetlem 8407  nvelbl 8409  nvcnpf 8412  nvlmle 8417  va1cnlem 8429  ipval2lem3 8439  ipval2 8441  4ipval2 8442  ipval3 8443  ipval2lem6 8445  nvcnpi3 8506  nvcnpi4 8507  nmoge0 8514  blometi 8547  htthlem8 8711  pslem 8731  psasym 8735  pstr 8736  spwcl 8744  efifolem6 8810  efif1lem1 8813  efif1lem2 8814  hvaddsub12 8990  hvsubdistr1 8999  hvsubdistr2 9000  hvaddcan2 9021  hvmulcan 9022  hvmulcan2 9023  hvsubcan 9024  hvsubcan2 9025  his7 9039  his2sub 9041  his2sub2 9042  norm3dif2 9101  hcau2 9138  shsubcl 9172  hhssnv 9217  shlej2 9439  pjspansn 9583  fh2 9645  cm2j 9646  pjoi0 9745  hosubdi 9817  unopf1o 9923  unopadj 9926  adj2 9941  braadd 9952  bramul 9953  lnopaddmuli 9980  lnopsubmuli 9982  nmcopexlem5 10038  lnfnaddmuli 10057  nmcfnexlem5 10067  adjlnop 10102  leopmul 10150  leoptr 10153  pjimai 10187  atcv1 10391  atexch 10392  atcvatlem 10396  lediv2aALT 10456  ghomf1olem 10481  fiiu 10535  fiiu2 10574  cnrsfin 10603  cnrscoa 10604  cmphmp 10615  hmphtr 10625  homcard 10633  neifil 10661  fgsb 10663  fgsb2 10668  eqidob 10805  cmphmia 10808  ismonc 10824  isepic 10834

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 154  df-an 232  df-3an 789

Copyright terms: Public domain