Theorem adantllr 433

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantllr

Step	Hyp	Ref	Expression
1		adantl2.1	. . . 4 |- (((ph /\ ps) /\ ch) -> th)
2	1	exp31 407	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	a1d 15	. 2 |- (ph -> (ta -> (ps -> (ch -> th))))
4	3	imp41 395	1 |- ((((ph /\ ta) /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  oewordri 5267  ordiso 5683  cnegexlem3 6501  cnegex 6502  lemul12b 7024  ser1add2i 7751  expmwordi 7851  seq1ublem 8163  bccl2 8223  fsumcmpndx2 8302  2climnn 8362  2climnn0 8363  climmullem3 8382  climcmpc1 8399  reccnv 8479  expcnv 8494  cvgratlem2 8513  cvgratlem5 8516  fsum0diag3 8522  tgcl 8894  tgss2 8907  neindisj 9007  iscncl 9047  blss 9130  metequiv 9158  metcnp 9165  lmle 9238  metelcls 9243  iscms2lem5 9271  bcthlem24 9300  bcthlem26 9302  grpidinvlem3 9330  grpideu 9333  grprcan 9347  blocni 9805  ubthlem3 9874  minveclem27 9916  minveclem28 9917  minveclem30 9919  minveclem31 9920  tx1cn 10223  normcan 11132  pjspansn 11133  unoplin 11481  hmoplin 11503  nmophmi 11598  lnopconi 11600  lnfnconi 11627  nlelchi 11631  mdslmd3i 11904  irredlem1 11962  irredlem2 11963  mdsymlem5 11979  cdj1i 12005  elicc3 15362  ordisoOLD 15374  neibastop3 15524  fmfnfmlem4 15597  difxp 15690  fzmul 15790  sdc 15811  fdc 15812  fdc1 15813  incsequz2 15816  mettrifi 15847  metdcn 15853  sstotbnd 15936  totbndss 15937  bndss 15942  totbndbnd 15944  ismtyhmeolem 15950  ismtybndlem 15952  heiborlem13 15967  heiborlem16 15970  heiborlem23 15977  heiborlem32 15986  heiborlem36 15990  rrncms 16019  rrntotbndlem1 16020  rrntotbnd 16022  ghomco 16040  phtpycom 16050  phtpycolem5 16055  pcohtpy 16083  rngisocnv 16135  ispridlc 16218  ps-1 17078  grpidinvlem3NEW 17111  grpideuNEW 17114  grprcanNEW 17122

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 164  df-an 242

Copyright terms: Public domain