Theorem ad2antlr 407

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 390	. 2 |- ((ch /\ ph) -> ps)
3	2	adantr 391	1 |- (((ch /\ ph) /\ th) -> ps)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  simplr 415  ax11eq 1369  ax11el 1370  tfindsg 3176  caoprord3 4072  oesuc 4180  oelim 4183  oaordi 4194  oaass 4209  odi 4224  omass 4225  oen0 4227  oelim2 4236  undom 4453  xpdom2 4457  mapenlem1 4504  mapenlem2 4505  php3 4530  fiint 4570  suppr 4600  fodom 4810  unxpdomlem 4856  npex 5104  elnp 5105  cnegext 5361  divdivdivt 5789  lemul12it 5848  lt2mul2divt 5877  lediv12it 5902  lediv2it 5903  xrmax2 5916  xrsupsslem 6082  xrinfmsslem 6083  xrub 6086  supxrre 6089  supxrun 6091  supxrunb1 6095  supxrunb2 6096  supxrbnd 6097  monoord 6305  elioc2t 6339  elico2t 6340  elicc2t 6341  elfzp1 6460  fsequb 6473  expnlbnd2t 6669  sqr11 6717  absmaxt 6911  seq1bnd 6924  cvganz 6938  caubnd 6940  facndivt 6957  faclbnd 6959  sumeq2 6999  fsumcmpndx2 7056  2climnn 7116  2climnn0 7117  climrecl 7124  climsqueeze 7154  climsqueeze2 7155  climsup 7169  climcau 7170  caucvglem6 7176  caucvg 7177  reccnv 7232  cvgratlem2 7265  cvgratlem3 7266  fsum0diaglem2 7271  fsum0diag4 7275  acdc3lem 7501  acdc2lem2 7504  acdc5lem2 7507  acdclem 7509  infxpidmlem12 7578  basgen2t 7651  elcls3 7720  islp2 7756  iscnp2 7770  cnpco 7778  blss 7862  metcnplem 7895  metcnp 7896  metcni2 7904  metcnp3 7905  metcnss2 7908  tgioolem 7923  lmnn 7944  metcnp4lem2 7978  metcn4 7980  xpcn 7985  bcthlem2 8009  bcthlem13 8020  bcthlem14 8021  bcthlem27 8034  bcthlem28 8035  grpidinv 8061  grpideu 8062  isgrp2i 8084  nvmul0or 8280  sm1cnilem 8355  sspval 8390  nmoub3i 8444  nmo0 8459  blocnilem 8472  blocni 8473  ipblnfi 8524  ubthlem3 8539  ubthlem5 8541  ubthlem13 8549  minveclem27 8579  minveclem31 8583  hvmul0ort 8901  hvaddsub4t 8952  occont 9167  ocorth 9171  occllem6 9185  projlem25 9217  osumlem4 9588  5oalem1 9606  5oalem2 9607  3oalem2 9615  pjds3 9665  nmopub2tALT 9840  nmfnleub2t 9857  hmopadj2t 9872  lnopcon 9970  lnfncon 9997  nlelch 10001  cnlnadjlem6 10012  kbass5t 10060  leopnmidt 10078  nmopleidt 10079  hmopidmch 10086  pjss2co 10099  pjssdif1 10110  pj3cor1 10145  mdsl0 10245  mdslmd1lem1 10260  mdslmd1lem2 10261  csmdsym 10269  superpos 10289  atoml 10317  irredlem2 10326  irredlem3 10327  atcvat3 10331  atcvat4 10332  mdsymlem5 10342  cdjreu 10367  cdj1 10368  cdrci 10500  cnrsfin 10515  cnrscoa 10516  mapdiscn 10517  sfvlim 10596  iintlem1 10623  trnij 10628  cmpasso 10697

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