Theorem ad2antlr 405

Description: Deduction adding conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant.1	|- (ph -> ps)

Assertion

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

Proof of Theorem ad2antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- (ph -> ps)
2	1	adantl 388	. 2 |- ((ch /\ ph) -> ps)
3	2	adantr 389	1 |- (((ch /\ ph) /\ th) -> ps)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  simplr 413  ax11eq 1356  ax11el 1357  tfindsg 3152  caoprord3 4044  oesuc 4150  oelim 4153  oaordi 4164  oaass 4179  odi 4194  omass 4195  oen0 4197  oelim2 4206  undom 4418  xpdom2 4422  mapenlem1 4469  mapenlem2 4470  php3 4495  fiint 4534  suppr 4562  fodom 4770  unxpdomlem 4815  npex 5063  elnp 5064  cnegext 5320  divdivdivt 5741  lemul12it 5800  lt2mul2divt 5822  lediv12it 5844  lediv2it 5845  xrmax2 5858  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxrre 6030  supxrun 6032  supxrunb1 6036  supxrunb2 6037  supxrbnd 6038  monoord 6231  elioc2t 6322  elico2t 6323  elicc2t 6324  elfzp1 6442  fsequb 6455  sqr11 6633  seq1bnd 6847  cvganz 6861  caubnd 6863  facndivt 6880  faclbnd 6882  sumeq2 6923  fsumcmpndx2 6980  2climnn 7039  2climnn0 7040  climrecl 7047  climsqueeze 7076  climsqueeze2 7077  climsup 7091  climcau 7092  caucvglem6 7098  caucvg 7099  reccnv 7153  cvgratlem2 7186  cvgratlem3 7187  fsum0diaglem2 7192  fsum0diag4 7196  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  infxpidmlem12 7506  basgen2t 7581  fctop 7592  elcls3 7652  islp2 7688  cnpco 7708  blss 7793  metcnplem 7825  metcnp 7826  metcni2 7834  metcnp3 7835  metcnss2 7838  tgioolem 7853  lmnn 7873  metcnp4lem2 7903  metcn4 7905  xpcn 7910  bcthlem2 7934  bcthlem13 7945  bcthlem14 7946  bcthlem27 7959  bcthlem28 7960  grpidinv 7986  grpideu 7987  isgrp2i 8011  nvmul0or 8212  sm1cnilem 8281  sspval 8316  nmoub3i 8368  nmo0 8383  blocnilem 8395  blocni 8396  ipblnfi 8447  ubthlem3 8462  ubthlem5 8464  ubthlem13 8472  minveclem27 8502  minveclem31 8506  hvmul0ort 8815  hvaddsub4t 8866  occont 9076  ocorth 9080  occllem6 9094  projlem25 9126  osumlem4 9498  5oalem1 9516  5oalem2 9517  3oalem2 9525  pjds3 9575  nmopub2tALT 9750  nmfnleub2t 9766  hmopadj2t 9781  lnopcon 9878  lnfncon 9905  nlelch 9909  cnlnadjlem6 9920  kbass5t 9965  leopnmidt 9982  nmopleidt 9983  hmopidmch 9990  pjss2co 10003  pjssdif1 10014  pj3cor1 10047  mdsl0 10145  mdslmd1lem1 10160  mdslmd1lem2 10161  csmdsym 10169  superpos 10189  atoml 10217  irredlem2 10226  irredlem3 10227  atcvat3 10231  atcvat4 10232  mdsymlem5 10242  cdjreu 10264  cdj1 10265  cdrci 10381  cnrsfin 10396  cnrscoa 10397  mapdiscn 10398  iintlem1 10476  trnij 10481  cmpasso 10550

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

Copyright terms: Public domain