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 1361  ax11el 1362  tfindsg 3157  caoprord3 4050  oesuc 4156  oelim 4159  oaordi 4170  oaass 4185  odi 4200  omass 4201  oen0 4203  oelim2 4212  undom 4424  xpdom2 4428  mapenlem1 4475  mapenlem2 4476  php3 4501  fiint 4540  suppr 4570  fodom 4778  unxpdomlem 4823  npex 5071  elnp 5072  cnegext 5328  divdivdivt 5749  lemul12it 5808  lt2mul2divt 5830  lediv12it 5852  lediv2it 5853  xrmax2 5866  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  supxrre 6038  supxrun 6040  supxrunb1 6044  supxrunb2 6045  supxrbnd 6046  monoord 6239  elioc2t 6330  elico2t 6331  elicc2t 6332  elfzp1 6450  fsequb 6463  sqr11 6641  seq1bnd 6855  cvganz 6869  caubnd 6871  facndivt 6888  faclbnd 6890  sumeq2 6931  fsumcmpndx2 6988  2climnn 7047  2climnn0 7048  climrecl 7055  climsqueeze 7084  climsqueeze2 7085  climsup 7099  climcau 7100  caucvglem6 7106  caucvg 7107  reccnv 7161  cvgratlem2 7194  cvgratlem3 7195  fsum0diaglem2 7200  fsum0diag4 7204  acdc3lem 7436  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  infxpidmlem12 7514  basgen2t 7589  fctop 7600  elcls3 7661  islp2 7697  iscnp2 7711  cnpco 7719  blss 7805  metcnplem 7838  metcnp 7839  metcni2 7847  metcnp3 7848  metcnss2 7851  tgioolem 7866  lmnn 7887  metcnp4lem2 7919  metcn4 7921  xpcn 7926  bcthlem2 7950  bcthlem13 7961  bcthlem14 7962  bcthlem27 7975  bcthlem28 7976  grpidinv 8002  grpideu 8003  isgrp2i 8026  nvmul0or 8224  sm1cnilem 8294  sspval 8329  nmoub3i 8381  nmo0 8396  blocnilem 8408  blocni 8409  ipblnfi 8460  ubthlem3 8475  ubthlem5 8477  ubthlem13 8485  minveclem27 8515  minveclem31 8519  hvmul0ort 8833  hvaddsub4t 8884  occont 9099  ocorth 9103  occllem6 9117  projlem25 9149  osumlem4 9521  5oalem1 9539  5oalem2 9540  3oalem2 9548  pjds3 9598  nmopub2tALT 9773  nmfnleub2t 9789  hmopadj2t 9804  lnopcon 9901  lnfncon 9928  nlelch 9932  cnlnadjlem6 9943  kbass5t 9991  leopnmidt 10009  nmopleidt 10010  hmopidmch 10017  pjss2co 10030  pjssdif1 10041  pj3cor1 10075  mdsl0 10174  mdslmd1lem1 10189  mdslmd1lem2 10190  csmdsym 10198  superpos 10218  atoml 10246  irredlem2 10255  irredlem3 10256  atcvat3 10260  atcvat4 10261  mdsymlem5 10271  cdjreu 10293  cdj1 10294  cdrci 10417  cnrsfin 10432  cnrscoa 10433  mapdiscn 10434  iintlem1 10512  trnij 10517  cmpasso 10586

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