Theorem 3adant3r3 1164

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3r3

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3expb 1154	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	3adantr3 1118	1 |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936

This theorem is referenced by:  ressress  13481  plttr  14382  plelttr  14384  joinle  14405  meetle  14412  latjle12  14446  latlem12  14462  latledi  14473  latmlej11  14474  latmlej21  14476  latmlej22  14477  latjass  14479  latj12  14480  latj31  14483  ipopos  14541  latdisdlem  14570  ismndd  14674  imasmnd2  14687  imasmnd  14688  grpaddsubass  14833  grpsubsub4  14836  grpnpncan  14838  imasgrp2  14888  imasgrp  14889  frgp0  15347  cmn12  15387  abladdsub  15394  imasrng  15680  dvrass  15750  lss1  15970  islmhm2  16069  psrgrp  16417  psrlmod  16420  zntoslem  16792  ipdir  16825  t1sep  17388  mettri2  18324  xmetrtri  18338  xmetrtri2  18339  pi1grplem  19027  dchrabl  20991  grpomuldivass  21790  grpopnpcan2  21794  grponpncan  21796  grpodiveq  21797  ablomuldiv  21830  ablodivdiv4  21832  nvadd12  22055  nvmdi  22084  nvsubadd  22089  nvmtri2  22114  dipdi  22297  dipsubdir  22302  dipsubdi  22303  ax5seglem4  25775  cgr3tr4  25890  cgr3rflx  25892  seglemin  25951  linerflx1  25987  elicc3  26210  rngosubdi  26459  rngosubdir  26460  igenval2  26566  dmncan1  26576  mendlmod  27369  latmassOLD  29712  omlfh1N  29741  omlfh3N  29742  cvrnbtwn  29754  cvrnbtwn2  29758  cvrnbtwn4  29762  hlatj12  29853  cvrntr  29907  islpln2a  30030  3atnelvolN  30068  elpadd2at2  30289  paddasslem17  30318  paddass  30320  paddssw2  30326  pmapjlln1  30337  ltrn2ateq  30662  cdlemc3  30675  cdleme1b  30708  cdleme3b  30711  cdleme3c  30712  cdleme9b  30734  erngdvlem3  31472  erngdvlem3-rN  31480  dvalveclem  31508

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938