Theorem 3adant2 797

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 785	. 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 774

This theorem is referenced by:  3ad2ant1 799  3adantl2 803  eupickb 1433  ordunel 3079  funopg 3539  fnco 3587  f1ocnvfvb 3872  oprssoprval 4025  curry1val 4090  oaord 4171  omcan 4190  omwordri 4193  odi 4200  oecan 4206  oewordri 4209  oeordsuc 4211  nnaordr 4226  ecopoprtrn 4301  eceqopreq 4303  fodomr 4469  ltsopi 4996  ltsopq 5055  ltsopr 5116  ltsosr 5183  ltasr 5189  adddirt 5299  addcan2t 5333  subcan2t 5382  subcant 5392  subdit 5407  subdirt 5408  nnncan1t 5447  pnpcan2t 5459  pnncant 5460  axlttrn 5484  letrt 5506  xrletrt 5545  ltadd2t 5606  leadd2t 5608  lesub1t 5641  lesub2t 5642  ltsub1t 5643  ltsub2t 5644  mulcan2t 5670  div13t 5714  ltmul2t 5795  lemul1t 5796  lemul2t 5797  lemul2it 5803  lemul2itOLD 5804  lt2mul2divt 5830  ltdiv2t 5843  lediv2t 5847  nndivtrt 5915  bndndx 6028  supxrbnd 6046  uzwo3lem1 6172  qsqueeze 6226  shftval2t 6292  iooss1 6318  iooss2 6319  ioossicc 6338  ioonegt 6347  iccnegt 6348  icoshft 6349  elfz2nn0t 6435  fzrev2it 6453  fzrevral2t 6460  fzshftralt 6462  expsubt 6537  expwordit 6542  expword2it 6544  expubndt 6547  bernneq2 6592  abs3dift 6844  seq1ub 6857  fsumshft 6977  fsumshftm 6978  caucvglem2 7102  isummulc1ALT 7156  cvgratlem5 7197  cncffvrn 7216  sin02gt0 7428  infxpidmlem4 7506  infxp 7523  istps3 7558  subbas2 7595  iincld 7629  neiint 7669  elnei 7675  islp2 7697  cnco 7718  cncnp 7728  cnconst 7730  metsym 7766  metge0 7771  metxplem3 7780  metxplem4 7785  blin 7804  ssbl 7807  metcnpf 7835  metcnp 7839  metcnpi3 7844  metcnpi4 7845  metcnss 7850  metcnss2 7851  cnmet 7856  dscmet 7870  lmuni 7902  metcnp4 7920  iscms2lem4 7942  isgrp 7991  grpinvid1 8022  grpinvid2 8023  grpasscan1 8027  grpinvop 8030  grpdivinv 8033  grpinvdiv 8034  grpdivf 8035  grppncan 8040  grpnpcan 8041  grppnpcan2 8042  resgrprn 8045  ablnncan 8064  vcnegsubdi2 8146  vcsub4 8147  nvmval 8215  nvmul0or 8224  nvsubadd 8227  nvpncan2 8228  nvaddsub4 8233  nvnncan 8235  nvmeq0 8236  nvdif 8245  nvpi 8246  nvmtri 8251  nvabs 8253  imsmetlem 8274  nvelbl 8276  nvlmle 8281  va1cnlem 8292  ipval2lem3 8302  ipval2 8304  4ipval2 8305  ipval3 8306  ipval2lem6 8308  nvcnpi4 8368  nmoge0 8375  blometi 8407  htthlem8 8570  pslem 8590  psasym 8593  pstr 8594  spwcl 8601  efifolem6 8661  efif1lem1 8664  efif1lem2 8665  hvaddsub12t 8846  hvsubdistr1t 8855  hvsubdistr2t 8856  hvaddcan2t 8877  hvmulcant 8878  hvmulcan2t 8879  hvsubcant 8880  hvsubcan2t 8881  his7t 8895  his2subt 8897  his2sub2t 8898  norm3dif2t 8957  hcau2 8994  shsubclt 9028  hhssnv 9073  shlej2t 9294  pjspansnt 9440  fh2t 9502  cm2jt 9503  pjoi0t 9602  hosubdit 9674  unopf1ot 9779  unopadjt 9782  adj2t 9797  braaddt 9808  bramult 9809  lnopaddmul 9836  lnopsubmul 9838  nmcopexlem5 9893  lnfnaddmul 9912  nmcfnexlem5 9922  adjlnopt 9957  leopmult 10005  leoptrt 10008  pjima 10042  atcv1t 10244  atexcht 10245  atcvatlem 10249  lediv2itALT 10305  ghomf1olem 10330  fiiu 10386  fiiu2 10413  cnrsfin 10432  cnrscoa 10433  cmphmp 10444  hmphtr 10454  homcard 10462  neifil 10478  fgsb 10480  fgsb2 10485  eqidob 10603  cmphmia 10606  ismonc 10620

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 776

Copyright terms: Public domain