Theorem 3adant2 798

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 786	. 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 775

This theorem is referenced by:  3ad2ant1 800  3adantl2 804  eupickb 1435  ordunel 3084  funopg 3547  fnco 3595  f1ocnvfvb 3881  oprssoprval 4034  curry1val 4100  oaord 4181  omcan 4200  omwordri 4203  odi 4210  oecan 4216  oewordri 4219  oeordsuc 4221  nnaordr 4236  ecopoprtrn 4311  eceqopreq 4313  fodomr 4483  ltsopi 5016  ltsopq 5075  ltsopr 5136  ltsosr 5203  ltasr 5209  adddirt 5319  addcan2t 5353  subcan2t 5402  subcant 5412  subdit 5427  subdirt 5428  nnncan1t 5467  pnpcan2t 5479  pnncant 5480  axlttrn 5504  letrt 5525  xrletrt 5564  ltadd2t 5624  leadd2t 5626  lesub1t 5660  lesub2t 5661  ltsub1t 5662  ltsub2t 5663  mulcan2t 5692  mulcan2tOLD 5693  div13t 5743  ltmul2t 5831  lemul1t 5832  lemul2t 5833  lemul2it 5839  lemul2itOLD 5840  lediv1t 5851  ltmuldiv2t 5865  lt2mul2divt 5872  lemuldivt 5874  lemuldiv2t 5876  ltdiv2t 5887  lediv2t 5891  nndivtrt 5960  bndndx 6073  supxrbnd 6091  uzwo3lem1 6216  qsqueeze 6280  shftval2t 6347  iooss1 6373  iooss2 6374  eliooordt 6388  ioonegt 6406  iccnegt 6407  icoshft 6408  ioojoint 6416  elfz2nn0t 6495  fzrev2it 6513  fzrevral2t 6520  fzshftralt 6522  expsubt 6598  expwordit 6603  expword2it 6605  expubndt 6608  bernneq2 6653  abs3dift 6899  seq1ub 6912  fsumshft 7031  fsumshftm 7032  caucvglem2 7158  isummulc1ALT 7213  cvgratlem5 7254  cncffvrn 7273  sin02gt0 7478  infxpidmlem4 7555  infxp 7572  istps3 7608  subbas2OLD 7645  iincld 7679  neiint 7719  elnei 7725  islp2 7747  cnco 7768  cncnp 7778  cnconst 7780  metsym 7816  metge0 7819  metxplem3 7828  metxplem4 7833  blin 7852  ssbl 7855  metcnpf 7883  metcnp 7887  metcnpi3 7892  metcnpi4 7893  metcnss 7898  metcnss2 7899  cnmet 7904  dscmet 7918  lmuni 7951  metcnp4 7970  iscms2lem4 7992  isgrp 8041  grpinvid1 8072  grpinvid2 8073  grpasscan1 8077  grpinvop 8080  grpdivinv 8083  grpinvdiv 8084  grpdivf 8085  grppncan 8090  grpnpcan 8091  grppnpcan2 8092  resgrprn 8095  ablnncan 8112  vcnegsubdi2 8194  vcsub4 8195  nvmval 8263  nvmul0or 8272  nvsubadd 8275  nvpncan2 8276  nvaddsub4 8281  nvnncan 8283  nvmeq0 8284  nvdif 8293  nvpi 8294  nvmtri 8299  nvabs 8301  imsmetlem 8323  nvelbl 8325  nvcnpf 8328  nvlmle 8333  va1cnlem 8345  ipval2lem3 8355  ipval2 8357  4ipval2 8358  ipval3 8359  ipval2lem6 8361  nvcnpi3 8422  nvcnpi4 8423  nmoge0 8430  blometi 8463  htthlem8 8627  pslem 8647  psasym 8651  pstr 8652  spwcl 8660  efifolem6 8727  efif1lem1 8730  efif1lem2 8731  hvaddsub12t 8907  hvsubdistr1t 8916  hvsubdistr2t 8917  hvaddcan2t 8938  hvmulcant 8939  hvmulcan2t 8940  hvsubcant 8941  hvsubcan2t 8942  his7t 8956  his2subt 8958  his2sub2t 8959  norm3dif2t 9018  hcau2 9055  shsubclt 9089  hhssnv 9134  shlej2t 9356  pjspansnt 9500  fh2t 9562  cm2jt 9563  pjoi0t 9662  hosubdit 9734  unopf1ot 9840  unopadjt 9843  adj2t 9858  braaddt 9869  bramult 9870  lnopaddmul 9897  lnopsubmul 9899  nmcopexlem5 9955  lnfnaddmul 9974  nmcfnexlem5 9984  adjlnopt 10019  leopmult 10067  leoptrt 10070  pjima 10104  atcv1t 10307  atexcht 10308  atcvatlem 10312  lediv2itALT 10371  ghomf1olem 10396  fiiu 10453  fiiuOLD 10454  fiiu2 10488  fiiu2OLD 10489  cnrsfin 10509  cnrscoa 10510  cmphmp 10521  hmphtr 10531  homcard 10539  neifil 10568  fgsb 10570  fgsbOLD 10571  fgsb2 10580  eqidob 10723  cmphmia 10726  ismonc 10742

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 777

Copyright terms: Public domain