Theorem adantrr 395

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
adant2.1	|- ((ph /\ ps) -> ch)

Assertion

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

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 373	. . 3 |- (ph -> (ps -> ch))
3	2	adantrd 391	. 2 |- (ph -> ((ps /\ th) -> ch))
4	3	imp 350	1 |- ((ph /\ (ps /\ th)) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ad2ant2r 409  ad2ant2lr 410  anabss1 499  3ad2antr1 812  sbcom 1258  ax11eq 1363  ax11el 1364  ifboth 2375  po2nr 2847  sotric 2860  tz7.7 2973  ordsucun 3082  opelxp1 3205  isocnv 3896  isomin 3899  isoini 3900  oalim 4167  omlim 4168  oaass 4195  omordi 4197  omwordri 4203  odi 4210  oen0 4213  oewordri 4219  oeworde 4220  dom2d 4404  ssenen 4504  ssfi 4537  ssfiOLD 4538  inf3lem6 4618  rankxplim3 4714  aceq5lem4 4738  aceq6b 4742  unidom 4808  axacndlem4 4962  ltapq 5076  ltmpq 5077  ltexpq 5080  ltexprlem6 5147  ssgt0sr 5217  add4t 5338  2addsubt 5389  mul4t 5420  muladdt 5421  xrlttrt 5553  ltleaddt 5645  rec11rt 5779  divdivdivt 5785  divdiv23t 5792  lemul2it 5839  lemul12ait 5842  ltmuldiv2t 5865  ltdivmult 5867  ltdivmul2t 5870  lemuldiv2t 5876  ltdiv23t 5892  lediv23t 5893  suprleub 6059  infmrcl 6069  xrsupsslem 6076  xrinfmsslem 6077  supxrunb1 6089  supxrunb2 6090  supxrleub 6099  zextltt 6190  zmax 6220  qbtwnre 6278  icounlem 6412  ioojoint 6416  recexpt 6595  expsubt 6598  expordit 6600  expord2t 6604  sqlecant 6641  lenegsqt 6885  seq1ublem 6911  fsumcom 7028  fsumshft 7031  2climnn 7102  2climnn0 7103  climge0 7112  climaddlem3 7116  climmullem1 7120  climmullem3 7122  climmullem5 7124  climmullem8 7127  climsqueeze 7140  climsqueeze2 7141  climcau 7156  serzf0 7169  ser1f0 7170  ser1cmp2 7177  cvgratlem2 7251  cvgratlem5 7254  fsum0diaglem2 7257  mulc1cncf 7279  acdc3lem 7486  acdclem 7494  infxpidmlem7 7558  infxpidmlem12 7563  eltg2t 7619  tgclt 7624  tgval3t 7625  tgss2t 7637  2basgent 7641  iscld 7669  ntrss 7688  ssnei2 7730  neindisj 7731  islp2 7747  cnpcl 7764  dnsconst 7788  ismsg 7800  blss 7853  blssex 7854  metcnp 7887  metcnpi3 7892  metcnpi4 7893  metcni2 7895  tgioolem 7914  lmss 7953  lmle 7960  metelcls 7965  metcnp4 7970  xplmi 7973  xpcn 7976  lmcau 7996  cmsss 7997  bcthlem11 8009  bcthlem15 8013  bcthlem18 8016  bcthlem19 8017  bcthlem20 8018  bcthlem21 8019  bcthlem24 8022  grpidinv 8052  grprcan 8063  grpinvid1 8072  grpinvid2 8073  grplcan 8075  abl4 8105  isring 8141  nvsubadd 8275  nvabs 8301  va1cnlem 8345  nvcnpi3 8422  nvcnpi4 8423  sspph 8515  ubthlem3 8531  ubthlem9 8537  ubthlem11 8539  ubthlem12 8540  ubthlem14 8542  hvadd4t 8905  hvaddsub4t 8945  chocuni 9172  occllem6 9178  shscl 9281  pjspansnt 9500  fh1t 9561  fh2t 9562  cm2jt 9563  spansncv 9597  5oalem2 9600  5oalem5 9603  5oalem6 9604  3oalem2 9608  hoadd4t 9710  cnvunopt 9842  bralnfnt 9872  eighmortht 9888  hmopst 9945  hmopmt 9946  hmopcot 9948  lnopcon 9963  lnfncon 9990  adjlnopt 10019  adjmult 10025  adjaddt 10026  nmopco 10028  kbass6t 10054  hstlet 10157  stles 10168  strlem3a 10179  hstrlem3a 10187  mdsl0 10237  mdexch 10262  atom1d 10280  superpos 10281  cvexchlem 10295  atoml 10309  atcvatlem 10312  irredlem2 10318  irredlem3 10319  atcvat4 10324  mdsymlem1 10330  mdsymlem3 10332  mdsymlem5 10334  mdsymlem6 10335  sumdmdlem 10345  sumdmdlem2 10346  cdj1 10360  cdj3lem2b 10364  nndivsub 10421

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