Theorem 3adant1 795

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

This theorem is referenced by:  3ad2ant2 799  3ad2ant3 800  3adantl1 801  sbciegft 1949  ordunel 3074  find 3145  funopg 3533  fvco 3759  eloprabg 3992  oaord 4165  oacan 4166  omord 4183  omcan 4184  omwordri 4187  odi 4194  omass 4195  oecan 4200  oewordri 4203  oeordsuc 4205  nnaordr 4220  nnmordi 4230  ecopoprtrn 4295  eceqopreq 4297  ixpf 4340  fodomr 4463  ltsopi 4988  genpass 5084  ltsopr 5108  adddirt 5291  add23t 5309  subsub23t 5348  addsubasst 5355  subcan2t 5374  subcant 5384  mul23t 5391  subdit 5399  subdirt 5400  subsub2t 5433  subsub4t 5436  sub23t 5437  nnncant 5438  nnncan2t 5440  nppcan2t 5442  pnpcan2t 5451  pnncant 5452  axlttrn 5476  ltletrt 5497  letrt 5498  xrltletrt 5536  xrletrt 5537  xrre2t 5543  ltadd2t 5598  leadd2t 5600  ltsubadd2t 5602  lesubadd2t 5604  lesub1t 5633  ltsub1t 5635  mulcan2t 5662  divmul3t 5678  divrec2t 5703  diveq0t 5724  divcan5t 5737  divdivmult 5751  ltmul2t 5787  lemul1t 5788  lemul2t 5789  lemul2it 5795  lemul2itOLD 5796  gt0divt 5807  ge0divt 5808  ltdivmult 5819  ledivmult 5820  ltdivmul2t 5821  lt2mul2divt 5822  ledivmul2t 5823  ltdiv23t 5840  lediv23t 5841  ledivp1 5854  ltdivp1 5855  xrltmint 5862  lemint 5869  nndivtrt 5907  uzind2 6154  nn0ind 6160  seq1rn2 6258  shftval2t 6284  iooss1 6310  ioossicc 6330  ioonegt 6339  iccnegt 6340  icoshft 6341  fzrev2it 6445  fzrev3t 6446  fzrevralt 6451  expsubt 6529  expordit 6531  expcant 6532  expordt 6533  expwordit 6534  expword2it 6536  abssubne0t 6820  absdifltt 6821  absdiflet 6822  abs3dift 6836  bcval2t 6897  fsumshftm 6970  fsummulc2 6972  climmullem3 7058  climmullem4 7059  climmullem5 7060  caucvglem2 7094  geoisum1c 7180  cvgratlem2ALT 7183  cvgratlem2 7186  clsss 7629  opnssneib 7670  islp2 7688  metxplem3 7768  metxplem4 7773  ssblex 7796  metcnpi3 7831  metcnpi4 7832  metcni2 7834  metcnss2 7838  dscmet 7856  bcthlem9 7941  bcthlem14 7946  grpdivval 8017  issubgi 8059  ablmul 8068  ghgrpilem4 8073  ghgrpi 8074  ringsn 8100  imsdval 8255  imsmetlem 8261  va1cnlem 8279  ipval 8287  nmoxr 8361  nmolb 8366  blometi 8394  phpar2 8413  phpar 8414  ipasslem5 8425  minveclem24 8499  minveclem25 8500  htthlem8 8557  pslem 8573  efgh 8633  efifolem5 8641  circgrpOLD 8658  hvadd23t 8824  hvaddsub12t 8828  hvaddsubasst 8831  hvsubdistr1t 8837  hvsubdistr2t 8838  hvmulcant 8860  hvmulcan2t 8861  hvsubcant 8862  his5t 8874  his2subt 8879  hcau2 8976  hhssnv 9054  shlej1t 9270  shlej2t 9271  pjoi0t 9579  hoadd23t 9626  hosubdit 9651  hosubsub2t 9655  hoaddsubasst 9658  hosubsub4t 9661  nmoplbt 9748  unopt 9755  hmopt 9762  nmfnlbt 9764  lnopmult 9807  nmcopexlem5 9870  nmcfnexlem5 9899  kbass1t 9961  kbass2t 9962  leopmul2it 9980  cvntrt 10129  mdslmd4 10168  mdexch 10170  atcv1t 10215  sumdmdi 10249  lediv2itALT 10276  symggrpiOLD 10311  symggrpi 10313  cayleylem2 10317  truni1 10386  cnrsfin 10396  cmphmp 10408  hmphtr 10418  hmeogrp 10425

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