Theorem 3adant1 796

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
3adant.1	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
3adant1	|- ((th /\ ph /\ ps) -> ch)

Proof of Theorem 3adant1

Step	Hyp	Ref	Expression
1		3simpc 786	. 2 |- ((th /\ ph /\ ps) -> (ph /\ ps))
2		3adant.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	syl 10	1 |- ((th /\ ph /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 774

This theorem is referenced by:  3ad2ant2 800  3ad2ant3 801  3adantl1 802  sbciegft 1955  ordunel 3079  find 3150  brelrng 3338  funopg 3539  fvco 3765  eloprabg 3998  oaord 4171  oacan 4172  omord 4189  omcan 4190  omwordri 4193  odi 4200  omass 4201  oecan 4206  oewordri 4209  oeordsuc 4211  nnaordr 4226  nnmordi 4236  ecopoprtrn 4301  eceqopreq 4303  ixpf 4346  fodomr 4469  ltsopi 4996  genpass 5092  ltsopr 5116  adddirt 5299  add23t 5317  subsub23t 5356  addsubasst 5363  subcan2t 5382  subcant 5392  mul23t 5399  subdit 5407  subdirt 5408  subsub2t 5441  subsub4t 5444  sub23t 5445  nnncant 5446  nnncan2t 5448  nppcan2t 5450  pnpcan2t 5459  pnncant 5460  axlttrn 5484  ltletrt 5505  letrt 5506  xrltletrt 5544  xrletrt 5545  xrre2t 5551  ltadd2t 5606  leadd2t 5608  ltsubadd2t 5610  lesubadd2t 5612  lesub1t 5641  ltsub1t 5643  mulcan2t 5670  divmul3t 5686  divrec2t 5711  diveq0t 5732  divcan5t 5745  divdivmult 5759  ltmul2t 5795  lemul1t 5796  lemul2t 5797  lemul2it 5803  lemul2itOLD 5804  gt0divt 5815  ge0divt 5816  ltdivmult 5827  ledivmult 5828  ltdivmul2t 5829  lt2mul2divt 5830  ledivmul2t 5831  ltdiv23t 5848  lediv23t 5849  ledivp1 5862  ltdivp1 5863  xrltmint 5870  lemint 5877  nndivtrt 5915  uzind2 6162  nn0ind 6168  seq1rn2 6266  shftval2t 6292  iooss1 6318  ioossicc 6338  ioonegt 6347  iccnegt 6348  icoshft 6349  fzrev2it 6453  fzrev3t 6454  fzrevralt 6459  expsubt 6537  expordit 6539  expcant 6540  expordt 6541  expwordit 6542  expword2it 6544  abssubne0t 6828  absdifltt 6829  absdiflet 6830  abs3dift 6844  bcval2t 6905  fsumshftm 6978  fsummulc2 6980  climmullem3 7066  climmullem4 7067  climmullem5 7068  caucvglem2 7102  geoisum1c 7188  cvgratlem2ALT 7191  cvgratlem2 7194  clsss 7637  opnssneib 7679  islp2 7697  metxplem3 7780  metxplem4 7785  ssblex 7808  metcnpi3 7844  metcnpi4 7845  metcni2 7847  metcnss2 7851  dscmet 7870  bcthlem9 7957  bcthlem14 7962  grpdivval 8032  issubgi 8074  ablmul 8083  ghgrpilem4 8088  ghgrpi 8089  ringsn 8115  imsdval 8268  imsmetlem 8274  va1cnlem 8292  ipval 8300  nmoxr 8374  nmolb 8379  blometi 8407  phpar2 8426  phpar 8427  ipasslem5 8438  minveclem24 8512  minveclem25 8513  htthlem8 8570  pslem 8590  efgh 8652  efifolem5 8660  circgrpOLD 8677  hvadd23t 8842  hvaddsub12t 8846  hvaddsubasst 8849  hvsubdistr1t 8855  hvsubdistr2t 8856  hvmulcant 8878  hvmulcan2t 8879  hvsubcant 8880  his5t 8892  his2subt 8897  hcau2 8994  hhssnv 9073  shlej1t 9293  shlej2t 9294  pjoi0t 9602  hoadd23t 9649  hosubdit 9674  hosubsub2t 9678  hoaddsubasst 9681  hosubsub4t 9684  nmoplbt 9771  unopt 9778  hmopt 9785  nmfnlbt 9787  lnopmult 9830  nmcopexlem5 9893  nmcfnexlem5 9922  kbass1t 9987  kbass2t 9988  leopmul2it 10006  leoptrt 10008  cvntrt 10157  mdslmd4 10197  mdexch 10199  atcv1t 10244  sumdmdi 10278  lediv2itALT 10305  symggrpi 10340  cayleylem2 10344  truni1 10422  cnrsfin 10432  cmphmp 10444  hmphtr 10454  hmeogrp 10461

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