Theorem 3adant1 809

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 799	. 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 230   /\ w3a 787

This theorem is referenced by:  3ad2ant2 813  3ad2ant3 814  3adantl1 815  sbciegft 2009  ordunel 3141  find 3212  brelrng 3400  relelrng 3404  funopg 3604  fvco 3831  eloprabg 4065  oaord 4239  oacan 4240  omord 4257  omcan 4258  omwordri 4261  odi 4268  omass 4269  oecan 4274  oewordri 4277  oeordsuc 4279  nnaordr 4294  nnmordi 4304  ecopoprtrn 4372  eceqopreq 4374  ixpf 4417  fodomr 4546  ltsopi 5081  genpass 5177  ltsopr 5201  adddir 5384  add23 5402  subsub23 5441  addsubass 5448  subcan2 5467  subcan 5477  mul23 5484  subdi 5492  subdir 5493  subsub2 5526  subsub4 5529  sub23 5530  nnncan 5531  nnncan2 5533  nppcan2 5535  pnpcan2 5544  pnncan 5545  axlttrn 5569  ltletr 5589  letr 5590  xrltletr 5628  xrletr 5629  xrre2 5635  ltadd2 5689  leadd2 5691  ltsubadd2 5693  lesubadd2 5695  lesub1 5725  ltsub1 5727  mulcan2 5757  mulcan2OLD 5758  divmul3 5776  divmul3OLD 5777  divrec2 5802  divass 5804  diveq0 5825  divsubdir 5832  divcan5 5839  divdivmul 5853  ltmul2 5889  lemul1 5890  lemul2 5891  lemul2a 5897  lemul2aOLD 5898  lediv1 5909  gt0div 5911  ge0div 5912  ltdivmul 5925  ltdivmulOLD 5926  ledivmul 5927  ledivmulOLD 5928  ltdivmul2 5929  ltdivmul2OLD 5930  lt2mul2div 5931  ledivmul2 5932  ledivmul2OLD 5933  lemuldiv 5934  ltdiv23 5952  lediv23 5953  ledivp1i 5966  ltdivp1i 5967  xrltmin 5974  lemin 5981  nndivtr 6021  uzind2 6291  nn0ind 6297  modcyc 6376  modcycOLD 6377  modcyc2 6378  modcyc2OLD 6379  iooss1 6398  eliooord 6413  iooneg 6432  iccneg 6433  icoshf 6434  ioojoin 6442  fzrev2i 6539  fzrev3 6540  fzrevral 6545  seq1rn2 6580  shftval2 6606  expsub 6687  expordi 6689  expcan 6690  expord 6691  expwordi 6692  expword2i 6694  mulre 6867  abssubne0 6972  absdiflt 6973  absdifle 6974  abs3dif 6989  bcval2 7049  fsumshftm 7122  fsummulc2 7124  climmullem3 7212  climmullem4 7213  climmullem5 7214  caucvglem2 7248  geoisum1c 7335  cvgratlem2ALT 7338  cvgratlem2 7341  clsss 7772  opnssneib 7814  islp2 7832  metxplem3 7913  metxplem4 7918  ssblex 7941  metcnpi3 7977  metcnpi4 7978  metcni2 7980  metcnss2 7984  dscmet 8003  bcthlem9 8092  bcthlem14 8097  grpdivval 8166  issubgi 8206  ablmul 8215  ghgrpilem4 8220  ghgrpi 8221  ringsn 8247  imsdval 8401  imsmetlem 8407  nvcni3 8415  va1cnlem 8429  ipval 8437  nmoxr 8513  nmolb 8518  blometi 8547  phpar2 8566  phpar 8567  ipasslem5 8578  minveclem24 8652  minveclem25 8653  htthlem8 8711  pslem 8731  efgh 8801  efifolem5 8809  hvadd23 8986  hvaddsub12 8990  hvaddsubass 8993  hvsubdistr1 8999  hvsubdistr2 9000  hvmulcan 9022  hvmulcan2 9023  hvsubcan 9024  his5 9036  his2sub 9041  hcau2 9138  hhssnv 9217  shlej1 9438  shlej2 9439  pjoi0 9745  hoadd23 9792  hosubdi 9817  hosubsub2 9821  hoaddsubass 9824  hosubsub4 9827  nmoplb 9914  unop 9922  hmop 9929  nmfnlb 9931  lnopmul 9974  nmcopexlem5 10038  nmcfnexlem5 10067  kbass1 10132  kbass2 10133  leopmul2i 10151  leoptr 10153  cvntr 10303  mdslmd4i 10344  mdexchi 10346  atcv1 10391  sumdmdii 10426  lediv2aALT 10456  symggrpi 10491  cayleylem2 10495  feq123 10568  truni1 10593  cnrsfin 10603  cmphmp 10615  hmphtr 10625  hmeogrp 10632  idfisf 10844

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 154  df-an 232  df-3an 789

Copyright terms: Public domain