Theorem 3adant2 796

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 784	. 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 223   /\ w3a 773

This theorem is referenced by:  3ad2ant1 798  3adantl2 802  eupickb 1428  ordunel 3074  funopg 3533  fnco 3581  f1ocnvfvb 3866  oprssoprval 4019  curry1val 4084  oaord 4165  omcan 4184  omwordri 4187  odi 4194  oecan 4200  oewordri 4203  oeordsuc 4205  nnaordr 4220  ecopoprtrn 4295  eceqopreq 4297  fodomr 4463  ltsopi 4988  ltsopq 5047  ltsopr 5108  ltsosr 5175  ltasr 5181  adddirt 5291  addcan2t 5325  subcan2t 5374  subcant 5384  subdit 5399  subdirt 5400  nnncan1t 5439  pnpcan2t 5451  pnncant 5452  axlttrn 5476  letrt 5498  xrletrt 5537  ltadd2t 5598  leadd2t 5600  lesub1t 5633  lesub2t 5634  ltsub1t 5635  ltsub2t 5636  mulcan2t 5662  div13t 5706  ltmul2t 5787  lemul1t 5788  lemul2t 5789  lemul2it 5795  lemul2itOLD 5796  lt2mul2divt 5822  ltdiv2t 5835  lediv2t 5839  nndivtrt 5907  bndndx 6020  supxrbnd 6038  uzwo3lem1 6164  qsqueeze 6218  shftval2t 6284  iooss1 6310  iooss2 6311  ioossicc 6330  ioonegt 6339  iccnegt 6340  icoshft 6341  elfz2nn0t 6427  fzrev2it 6445  fzrevral2t 6452  fzshftralt 6454  expsubt 6529  expwordit 6534  expword2it 6536  expubndt 6539  bernneq2 6584  abs3dift 6836  seq1ub 6849  fsumshft 6969  fsumshftm 6970  caucvglem2 7094  isummulc1ALT 7148  cvgratlem5 7189  cncffvrn 7208  sin02gt0 7420  infxpidmlem4 7498  infxp 7515  istps3 7550  subbas2 7587  iincld 7621  neiint 7660  elnei 7666  islp2 7688  cnco 7707  cncnp 7717  cnconst 7719  metsym 7755  metge0 7760  metxplem3 7768  metxplem4 7773  blin 7792  ssbl 7795  metcnpf 7822  metcnp 7826  metcnpi3 7831  metcnpi4 7832  metcnss 7837  metcnss2 7838  cnmet 7843  dscmet 7856  lmuni 7886  metcnp4 7904  iscms2lem4 7926  isgrp 7975  grpinvid1 8006  grpinvid2 8007  grpasscan1OLD 8008  grpasscan1 8012  grpinvop 8015  grpdivinv 8018  grpinvdiv 8019  grpdivf 8020  grppncan 8025  grpnpcan 8026  grppnpcan2 8027  resgrprn 8030  ablnncan 8049  vcnegsubdi2 8131  vcsub4 8132  nvmval 8203  nvmul0or 8212  nvsubadd 8215  nvpncan2 8216  nvaddsub4 8221  nvnncan 8223  nvmeq0 8224  nvdif 8232  nvpi 8233  nvmtri 8238  nvabs 8240  imsmetlem 8261  nvelbl 8263  nvlmle 8268  va1cnlem 8279  ipval2lem3 8289  ipval2 8291  4ipval2 8292  ipval3 8293  ipval2lem6 8295  nvcnpi4 8355  nmoge0 8362  blometi 8394  htthlem8 8557  pslem 8573  psasym 8576  spwcl 8583  efifolem6 8642  efif1lem1 8645  efif1lem2 8646  hvaddsub12t 8828  hvsubdistr1t 8837  hvsubdistr2t 8838  hvaddcan2t 8859  hvmulcant 8860  hvmulcan2t 8861  hvsubcant 8862  hvsubcan2t 8863  his7t 8877  his2subt 8879  his2sub2t 8880  norm3dif2t 8939  hcau2 8976  shsubclt 9010  hhssnv 9054  shlej2t 9271  pjspansnt 9417  fh2t 9479  cm2jt 9480  pjoi0t 9579  hosubdit 9651  unopf1ot 9756  unopadjt 9759  adj2t 9774  braaddt 9785  bramult 9786  lnopaddmul 9813  lnopsubmul 9815  nmcopexlem5 9870  lnfnaddmul 9889  nmcfnexlem5 9899  adjlnopt 9934  leopmult 9979  pjima 10015  atcv1t 10215  atexcht 10216  atcvatlem 10220  lediv2itALT 10276  ghomf1olem 10301  fiiu 10350  fiiu2 10377  cnrsfin 10396  cnrscoa 10397  cmphmp 10408  hmphtr 10418  homcard 10426  neifil 10442  fgsb 10444  fgsb2 10449  eqidob 10567  cmphmia 10570  ismonc 10584

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 147  df-an 225  df-3an 775

Copyright terms: Public domain